packages feed

cpsa-3.3.0: doc/examples/or.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.2.2 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Otway-Rees 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;Otway-Rees Protocol&quot;
  (comment &quot;Standard version using variables of sort mesg&quot;))
(comment &quot;CPSA 3.2.2&quot;)
(comment &quot;All input read from or.scm&quot;)</pre>

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

<div>
 <svg
  class='diagram' width='229.680pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 229.680 454.920' font-size='12.000'>
  <text
   x='189.720' y='401.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k9&quot;, &quot;_self&quot;)'>9</text>
  <line
   x1='139.800' y1='339.960' x2='189.720' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='326.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k8&quot;, &quot;_self&quot;)'>8</text>
  <line
   x1='139.800' y1='339.960' x2='189.720' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='251.040'
   style='font-style: italic; text-anchor: middle; fill: green;'
   onclick='window.open(&quot;#k6&quot;, &quot;_self&quot;)'>6</text>
  <line
   x1='139.800' y1='339.960' x2='189.720' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='326.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  <line
   x1='89.880' y1='339.960' x2='139.800' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='326.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</text>
  <line
   x1='39.960' y1='227.460' x2='89.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='176.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k7&quot;, &quot;_self&quot;)'>7</text>
  <line
   x1='139.800' y1='114.960' x2='189.720' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='101.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k6&quot;, &quot;_self&quot;)'>6</text>
  <line
   x1='139.800' y1='114.960' x2='189.720' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='26.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='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='101.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k3&quot;, &quot;_self&quot;)'>3</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;#k1&quot;, &quot;_self&quot;)'>1</text>
  <line
   x1='39.960' y1='227.460' x2='89.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='213.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol or basic
  (defrole init
    (vars (a b s name) (na text) (k skey) (m text))
    (trace (send (cat m a b (enc na m a b (ltk a s))))
      (recv (cat m (enc na k (ltk a s))))))
  (defrole resp
    (vars (a b s name) (nb text) (k skey) (m text) (x y mesg))
    (trace (recv (cat m a b x))
      (send (cat m a b x (enc nb m a b (ltk b s))))
      (recv (cat m y (enc nb k (ltk b s)))) (send y)))
  (defrole serv
    (vars (a b s name) (na nb text) (k skey) (m text))
    (trace
      (recv
        (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
      (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
    (uniq-orig k)))</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>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk b s)))</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat m a b x (enc nb m a b (ltk b s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a b x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))</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;'>or 0</text>
  </svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb)
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (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='189.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='339.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>(cat m-0 (enc na k (ltk a-0 s)) (enc nb k (ltk b s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m-0 a-0 b (enc na m-0 a-0 b (ltk a-0 s)) (enc nb m-0 a-0 b (ltk b s)))</title>
   <circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk b s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a b x (enc nb m a b (ltk b s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a b x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((na na) (nb nb) (m m-0) (a a-0) (b b) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))</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;'>or 1</text>
  </svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m na m-0 text) (s a b a-0 name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m-0) (a a-0) (b b) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (ltk b s))
    (0 2))
  (label 1)
  (parent 0)
  (unrealized (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='189.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='339.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>(cat m-0 (enc nb k (ltk b s)) (enc nb-0 k (ltk b-0 s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m-0 b b-0 (enc nb m-0 b b-0 (ltk b s)) (enc nb-0 m-0 b b-0 (ltk b-0 s)))</title>
   <circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk b s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a b x (enc nb m a b (ltk b s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a b x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((na nb) (nb nb-0) (m m-0) (a b) (b b-0) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))</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;'>or 2</text>
  </svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m nb-0 m-0 text) (s a b b-0 name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m-0) (a b) (b b-0) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (ltk b s))
    (0 2))
  (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>, Children: <a href="#k5">5</a> <a href="#k6">6</a> <a href="#k7">7</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='189.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='339.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>(cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s)))</title>
   <circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk b s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a b x (enc nb m a b (ltk b s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a b x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((na na) (nb nb) (m m) (a a) (b b) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))</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;'>or 3</text>
  </svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 a-0 b (ltk b s)) (1 0))
  (label 3)
  (parent 1)
  (unrealized (1 0))
  (comment &quot;3 in cohort - 3 not yet seen&quot;))</pre>

<p id="k4">Item <a href="#t0">4</a>, Parent: <a href="#k2">2</a>, Children: <a href="#k8">8</a> <a href="#k9">9</a>, Seen Child: <a href="#k6">6</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='189.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='339.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>(cat m (enc nb k (ltk a s)) (enc nb-0 k (ltk a s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (ltk a s)) (enc nb-0 m a a (ltk a s)))</title>
   <circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk a s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x (enc nb m a a (ltk a s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))</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;'>or 4</text>
  </svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m nb-0 text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 b b (ltk b s)) (1 0))
  (label 4)
  (parent 2)
  (seen 6)
  (unrealized (1 0))
  (comment &quot;3 in cohort - 2 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='279.840pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 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='239.880' y1='114.960' x2='239.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.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='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 114.960 Q 192.300 150.660 144.719 186.359'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a b (enc na m a b (ltk a s)))</title>
   <circle cx='239.880' cy='114.960' r='6.000'/></g>
  <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>(cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s)))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk b s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a b x (enc nb m a b (ltk b s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a b x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((na na) (m m) (a a) (b b) (s s))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((na na) (nb nb) (m m) (a a) (b b) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='139.920' y='39.960'
   style='text-anchor: middle;'>or 5 (realized)</text></svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  (defstrand init 1 (na na) (m m) (a a) (b b) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc na m a b (ltk a s)) (1 0))
  (label 5)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b b) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))</pre>

<p id="k6">Item <a href="#t0">6</a>, Parent: <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='189.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='339.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>(cat m (enc nb k (ltk a s)) (enc nb k (ltk a s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (ltk a s)) (enc nb m a a (ltk a s)))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk a s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x (enc nb m a a (ltk a s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((na nb) (nb nb) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))</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;'>or 6 (realized)</text></svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a s))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc na m a a (ltk a s)) (1 0))
  (label 6)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))</pre>

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

<div>
 <svg
  class='diagram' width='279.840pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 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='239.880' y1='114.960' x2='239.880' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.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='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x-0 (enc na m a a (ltk a s)))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x-0)</title>
   <circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
  <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>(cat m (enc na k (ltk a s)) (enc nb k (ltk a s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc na m a a (ltk a s)) (enc nb m a a (ltk a s)))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk a s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x (enc nb m a a (ltk a s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((x x-0) (nb na) (m m) (a a) (b a) (s s))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((na na) (nb nb) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='139.920' y='39.960'
   style='text-anchor: middle;'>or 7 (realized)</text></svg></div>

<pre>(defskeleton or
  (vars (x y x-0 mesg) (nb m na text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand resp 2 (x x-0) (nb na) (m m) (a a) (b a) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc na m a a (ltk a s)) (1 0))
  (label 7)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))</pre>

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

<div>
 <svg
  class='diagram' width='279.840pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 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='239.880' y1='114.960' x2='239.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.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='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 114.960 Q 192.300 150.660 144.719 186.359'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a (enc nb-0 m a a (ltk a s)))</title>
   <circle cx='239.880' cy='114.960' r='6.000'/></g>
  <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>(cat m (enc nb k (ltk a s)) (enc nb-0 k (ltk a s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (ltk a s)) (enc nb-0 m a a (ltk a s)))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk a s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x (enc nb m a a (ltk a s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((na nb-0) (m m) (a a) (b a) (s s))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='139.920' y='39.960'
   style='text-anchor: middle;'>or 8 (realized)</text></svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m nb-0 text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  (defstrand init 1 (na nb-0) (m m) (a a) (b a) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (ltk a s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc nb-0 m a a (ltk a s)) (1 0))
  (label 8)
  (parent 4)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))</pre>

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

<div>
 <svg
  class='diagram' width='279.840pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 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='239.880' y1='114.960' x2='239.880' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.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='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x-0 (enc nb-0 m a a (ltk a s)))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x-0)</title>
   <circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
  <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>(cat m (enc nb k (ltk a s)) (enc nb-0 k (ltk a s)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (ltk a s)) (enc nb-0 m a a (ltk a s)))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (ltk a s)))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat m a a x (enc nb m a a (ltk a s)))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a a x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((x x-0) (nb nb-0) (m m) (a a) (b a) (s s))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g><title>((x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='139.920' y='39.960'
   style='text-anchor: middle;'>or 9 (realized)</text></svg></div>

<pre>(defskeleton or
  (vars (x y x-0 mesg) (nb m nb-0 text) (s a name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b a) (s s) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  (defstrand resp 2 (x x-0) (nb nb-0) (m m) (a a) (b a) (s s))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a s))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc nb-0 m a a (ltk a s)) (1 0))
  (label 9)
  (parent 4)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  (origs (k (1 1)) (nb (0 1))))</pre>

</body>
</html>