ns.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.4.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Needham-Schroeder Public-Key Protocol</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;Needham-Schroeder Public-Key Protocol&quot;
  (comment &quot;This protocol contains a man-in-the-middle&quot;
    &quot;attack discovered by Galvin Lowe.&quot;))
(comment &quot;CPSA 3.4.0&quot;)
(comment &quot;All input read from ns.scm&quot;)</pre>

<p id="top">Trees: <a href="#t0">0</a> <a href="#t3">3</a>.</p>

<p id="t0">Tree <a href="#top">0</a>.</p>

<div>
 <svg
  class='diagram' width='179.760pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.760 79.920' font-size='12.000'>
  <text
   x='139.800' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</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='39.960' x2='89.880' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))))
  (comment &quot;Needham-Schroeder&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='79.920pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 304.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='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n2 (pubk b))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 (pubk a))</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 a (pubk b))</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 0</text>
  </svg></div>

<pre>(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (comment &quot;Initiator point-of-view&quot;)
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='179.880pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 304.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='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <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>(enc n1 n2-0 (pubk a))</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 a (pubk b))</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(enc n2 (pubk b))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n1 a (pubk b))</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 1</text>
  </svg></div>

<pre>(defskeleton ns
  (vars (n1 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (operation nonce-test (added-strand resp 2) n1 (0 1)
    (enc n1 a (pubk b)))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='179.880pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 304.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='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 189.960 Q 92.940 189.960 45.960 189.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n1 n2 (pubk a))</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 a (pubk b))</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(enc n2 (pubk b))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n1 a (pubk b))</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 2 (realized)</text></svg></div>

<pre>(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
  (label 2)
  (parent 1)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  (origs (n1 (0 0))))</pre>

<p id="t3">Tree <a href="#top">3</a>.</p>

<div>
 <svg
  class='diagram' width='129.840pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 129.840 79.920' font-size='12.000'>
  <text
   x='89.880' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  <line
   x1='39.960' y1='39.960' x2='89.880' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k3&quot;, &quot;_self&quot;)'>3</text>
  </svg></div>

<pre>(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))))
  (comment &quot;Needham-Schroeder&quot;))</pre>

<p id="k3">Item <a href="#t3">3</a>, Child: <a href="#k4">4</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 304.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='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n2 (pubk b))</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 (pubk a))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 a (pubk b))</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text x='39.960' y='39.960' style='text-anchor: middle;'>ns 3</text>
  </svg></div>

<pre>(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (comment &quot;Responder point-of-view&quot;)
  (label 3)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k4">Item <a href="#t3">4</a>, Parent: <a href="#k3">3</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 304.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='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 264.960 Q 92.940 264.960 45.960 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n2 (pubk b-0))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 (pubk a))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 a (pubk b-0))</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(enc n2 (pubk b))</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc n1 n2 (pubk a))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 a (pubk b))</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>ns 4 (realized)</text></svg></div>

<pre>(defskeleton ns
  (vars (n2 n1 text) (a b b-0 name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 (pubk a)))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  (origs (n2 (0 1))))</pre>

</body>
</html>