plaindh.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.2.1 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Plain diffie-hellman protocol with challenge-response</title>
 <meta http-equiv="content-type" content="application/xhtml+xml; charset=UTF-8" />
 <style>
  svg.diagram { border-width: 1px; border-style: solid }
 </style>
</head>
<body>

<pre>(herald &quot;Plain diffie-hellman protocol with challenge-response&quot;
  (algebra diffie-hellman))
(comment &quot;CPSA 3.2.1&quot;)
(comment &quot;All input read from plaindh.scm&quot;)</pre>

<p id="t0">Tree 0.</p>

<div>
 <svg
  class='diagram' width='229.680pt' height='154.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 229.680 154.920' font-size='12.000'>
  <text
   x='189.720' y='101.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k5&quot;, &quot;_self&quot;)'>5</text>
  <line
   x1='139.800' y1='114.960' x2='189.720' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='101.040' style='text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  <line
   x1='89.880' y1='114.960' x2='139.800' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='101.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</text>
  <line
   x1='39.960' y1='77.460' x2='89.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k3&quot;, &quot;_self&quot;)'>3</text>
  <line
   x1='89.880' y1='39.960' x2='139.800' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k1&quot;, &quot;_self&quot;)'>1</text>
  <line
   x1='39.960' y1='77.460' x2='89.880' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='63.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol plaindh diffie-hellman
  (defrole init
    (vars (x expn) (h base) (n text))
    (trace (send (exp (gen) x)) (recv h) (send (enc n (exp h x)))
      (recv n))
    (uniq-orig n)
    (uniq-gen x))
  (defrole resp
    (vars (y expn) (h base) (n text))
    (trace (recv h) (send (exp (gen) y)) (recv (enc n (exp h y)))
      (send n))
    (uniq-gen y)
    (ind-zero-in (y h)))
  (comment &quot;Diffie-hellman key exchange followed by an encryption&quot;))</pre>

<p id="k0">Item <a href="#t0">0</a>, Children: <a href="#k1">1</a> <a href="#k2">2</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp h x))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>h</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (h h) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960' style='text-anchor: middle;'>plaindh 0</text>
  </svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (h base) (x expn))
  (defstrand init 4 (n n) (h h) (x x))
  (uniq-gen x)
  (uniq-orig n)
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n)))
  (label 0)
  (unrealized (0 3))
  (origs (n (0 2)))
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k1">Item <a href="#t0">1</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k3">3</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>n</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp h (mul x y)))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 189.960 Q 92.940 189.960 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) y)</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp h x)</title>
   <circle style='fill: red;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>n</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 86.940 264.960 133.920 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n (exp h (mul x y)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(exp h y)</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (h (exp h x)) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n n) (h (exp h y)) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='89.940' y='39.960' style='text-anchor: middle;'>plaindh 1</text>
  </svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (h base) (x y expn))
  (defstrand init 4 (n n) (h (exp h y)) (x x))
  (defstrand resp 4 (n n) (h (exp h x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (ind-zero-in (y (exp h x)))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 4) n (0 3)
    (enc n (exp h (mul x y))))
  (traces
    ((send (exp (gen) x)) (recv (exp h y))
      (send (enc n (exp h (mul x y)))) (recv n))
    ((recv (exp h x)) (send (exp (gen) y))
      (recv (enc n (exp h (mul x y)))) (send n)))
  (label 1)
  (parent 0)
  (unrealized (0 1) (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k2">Item <a href="#t0">2</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k4">4</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 189.960 Q 91.604 262.464 43.287 334.967'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp h x)</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp h x)</title>
   <circle style='fill: red;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>n</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp h x))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>h</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (h h) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='89.940' y='39.960' style='text-anchor: middle;'>plaindh 2</text>
  </svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (h base) (x expn))
  (defstrand init 4 (n n) (h h) (x x))
  (deflistener (exp h x))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)))
  (uniq-gen x)
  (uniq-orig n)
  (operation nonce-test (added-listener (exp h x)) n (0 3)
    (enc n (exp h x)))
  (traces
    ((send (exp (gen) x)) (recv h) (send (enc n (exp h x))) (recv n))
    ((recv (exp h x)) (send (exp h x))))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k3">Item <a href="#t0">3</a>, Parent: <a href="#k1">1</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>n</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp (gen) (mul x y x-0)))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 189.960 Q 92.940 189.960 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) y)</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>n</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 86.940 264.960 133.920 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n (exp (gen) (mul x y x-0)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul y x-0))</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (h (exp (gen) (mul x x-0))) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n n) (h (exp (gen) (mul y x-0))) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>plaindh 3 (realized)</text></svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (x y expn) (x-0 expr))
  (defstrand init 4 (n n) (h (exp (gen) (mul y x-0))) (x x))
  (defstrand resp 4 (n n) (h (exp (gen) (mul x x-0))) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (ind-zero-in (y (exp (gen) (mul x x-0))))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (algebra-contracted (h (exp (gen) x-0)))
    (exp (gen) (mul x x-0)) (1 0) (exp (gen) x))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) (mul y x-0)))
      (send (enc n (exp (gen) (mul x y x-0)))) (recv n))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul x y x-0)))) (send n)))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps ((0) ((x x) (h (exp (gen) (mul y x-0))) (n n))))
  (origs (n (0 2))))</pre>

<p id="k4">Item <a href="#t0">4</a>, Parent: <a href="#k2">2</a>, Child: <a href="#k5">5</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 189.960 Q 91.604 262.464 43.287 334.967'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>n</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) x-0)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (h (exp (gen) x-0)) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>plaindh 4 (realized)</text></svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (x expn) (x-0 expr))
  (defstrand init 4 (n n) (h (exp (gen) x-0)) (x x))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (1 0)) ((1 1) (0 3)))
  (uniq-gen x)
  (uniq-orig n)
  (operation nonce-test (algebra-contracted (h (exp (gen) x-0)))
    (exp (gen) (mul x x-0)) (1 0) (exp (gen) x))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))) (recv n))
    ((recv (exp (gen) (mul x x-0))) (send (exp (gen) (mul x x-0)))))
  (label 4)
  (parent 2)
  (unrealized)
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k5">Item <a href="#t0">5</a>, Parent: <a href="#k4">4</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) x-0)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (h (exp (gen) x-0)) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960'
   style='text-anchor: middle;'>plaindh 5 (realized)</text></svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (x expn) (x-0 expr))
  (defstrand init 4 (n n) (h (exp (gen) x-0)) (x x))
  (uniq-gen x)
  (uniq-orig n)
  (operation generalization deleted (1 0))
  (traces
    ((send (exp (gen) x)) (recv (exp (gen) x-0))
      (send (enc n (exp (gen) (mul x x-0)))) (recv n)))
  (label 5)
  (parent 4)
  (unrealized)
  (shape)
  (maps ((0) ((x x) (h (exp (gen) x-0)) (n n))))
  (origs (n (0 2))))</pre>

</body>
</html>