packages feed

cpsa-3.4.0: doc/examples/bltk_or.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.4.0 -->
<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;)
  (algebra diffie-hellman))
(comment &quot;CPSA 3.4.0&quot;)
(comment &quot;All input read from bltk_or.scm&quot;)</pre>

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

<div>
 <svg
  class='diagram' width='279.600pt' height='829.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.600 829.920' font-size='12.000'>
  <text
   x='189.720' y='776.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k16&quot;, &quot;_self&quot;)'>16</text>
  <line
   x1='139.800' y1='714.960' x2='189.720' y2='789.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='701.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k15&quot;, &quot;_self&quot;)'>15</text>
  <line
   x1='139.800' y1='714.960' x2='189.720' y2='714.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='626.040'
   style='font-style: italic; text-anchor: middle; fill: green;'
   onclick='window.open(&quot;#k13&quot;, &quot;_self&quot;)'>13</text>
  <line
   x1='139.800' y1='714.960' x2='189.720' y2='639.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='701.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k8&quot;, &quot;_self&quot;)'>8</text>
  <line
   x1='89.880' y1='714.960' x2='139.800' y2='714.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='701.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  <line
   x1='39.960' y1='414.960' x2='89.880' y2='714.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='551.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k7&quot;, &quot;_self&quot;)'>7</text>
  <line
   x1='89.880' y1='564.960' x2='139.800' y2='564.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='551.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k3&quot;, &quot;_self&quot;)'>3</text>
  <line
   x1='39.960' y1='414.960' x2='89.880' y2='564.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='476.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k14&quot;, &quot;_self&quot;)'>14</text>
  <line
   x1='139.800' y1='377.460' x2='189.720' y2='489.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='401.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k13&quot;, &quot;_self&quot;)'>13</text>
  <line
   x1='139.800' y1='377.460' 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;#k12&quot;, &quot;_self&quot;)'>12</text>
  <line
   x1='139.800' y1='377.460' 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;#k10&quot;, &quot;_self&quot;)'>10</text>
  <line
   x1='139.800' y1='377.460' x2='189.720' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='363.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k6&quot;, &quot;_self&quot;)'>6</text>
  <line
   x1='89.880' y1='377.460' x2='139.800' y2='377.460'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='363.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</text>
  <line
   x1='39.960' y1='414.960' x2='89.880' y2='377.460'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='176.040'
   style='font-style: italic; text-anchor: middle; fill: green;'
   onclick='window.open(&quot;#k13&quot;, &quot;_self&quot;)'>13</text>
  <line
   x1='189.720' y1='189.960' x2='239.640' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='176.040' style='text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k11&quot;, &quot;_self&quot;)'>11</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;#k10&quot;, &quot;_self&quot;)'>10</text>
  <line
   x1='139.800' y1='114.960' x2='189.720' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='26.040'
   style='font-style: italic; text-anchor: middle; fill: green;'
   onclick='window.open(&quot;#k12&quot;, &quot;_self&quot;)'>12</text>
  <line
   x1='189.720' y1='39.960' x2='239.640' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='26.040' style='text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k9&quot;, &quot;_self&quot;)'>9</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;#k5&quot;, &quot;_self&quot;)'>5</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='414.960' x2='89.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='401.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol or diffie-hellman
  (defrole init
    (vars (a b s name) (na text) (k skey) (m text))
    (trace (send (cat m a b (enc na m a b (bltk a s))))
      (recv (cat m (enc na k (bltk 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 (bltk b s))))
      (recv (cat m y (enc nb k (bltk 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 (bltk a s)) (enc nb m a b (bltk b s))))
      (send (cat m (enc na k (bltk a s)) (enc nb k (bltk 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> <a href="#k3">3</a> <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>y</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat m y (enc nb k (bltk s b)))</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 (bltk s b)))</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 (bltk s a) (bltk s b))
  (uniq-orig nb)
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment &quot;4 in cohort - 4 not yet seen&quot;))</pre>

<p id="k1">Item <a href="#t0">1</a>, Parent: <a href="#k0">0</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='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 (bltk b a-0)) (enc nb k (bltk s b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m-0 a-0 s (enc na m-0 a-0 s (bltk b a-0)) (enc nb m-0 a-0 s (bltk s b)))</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 (bltk s 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-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 (bltk s b)))</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 s) (s b) (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 s) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (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="#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-0 (enc na k (bltk s a-0)) (enc nb k (bltk s b)))</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 (bltk s a-0)) (enc nb m-0 a-0 b (bltk s b)))</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 (bltk s 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-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 (bltk s b)))</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 2</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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (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="#k0">0</a>, Child: <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-0 (enc nb k (bltk s b)) (enc nb-0 k (bltk b b-0)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m-0 s b-0 (enc nb m-0 s b-0 (bltk s b)) (enc nb-0 m-0 s b-0 (bltk b b-0)))</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 (bltk s 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-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 (bltk s b)))</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 s) (b b-0) (s b) (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 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 s) (b b-0) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (0 2))
  (label 3)
  (parent 0)
  (unrealized (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k4">Item <a href="#t0">4</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k8">8</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 (bltk s b)) (enc nb-0 k (bltk s b-0)))</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 (bltk s b)) (enc nb-0 m-0 b b-0 (bltk s b-0)))</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 (bltk s 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-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 (bltk s b)))</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 4</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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand serv 2) (enc nb k (bltk s b))
    (0 2))
  (label 4)
  (parent 0)
  (unrealized (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k5">Item <a href="#t0">5</a>, Parent: <a href="#k1">1</a>, Children: <a href="#k9">9</a> <a href="#k10">10</a> <a href="#k11">11</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 (bltk a b)) (enc nb k (bltk b b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (bltk a b)) (enc nb m a b (bltk b b)))</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 (bltk b 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-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 (bltk b b)))</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 b) (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 b) (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 5</text>
  </svg></div>

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

<p id="k6">Item <a href="#t0">6</a>, Parent: <a href="#k2">2</a>, Children: <a href="#k12">12</a> <a href="#k13">13</a> <a href="#k14">14</a>, Seen Child: <a href="#k10">10</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 (bltk s a)) (enc nb k (bltk s b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (bltk s a)) (enc nb m a b (bltk s b)))</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 (bltk s 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-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 (bltk s b)))</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 6</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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 a-0 b (bltk s b)) (1 0))
  (label 6)
  (parent 2)
  (seen 10)
  (unrealized (1 0))
  (comment &quot;4 in cohort - 3 not yet seen&quot;))</pre>

<p id="k7">Item <a href="#t0">7</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 (bltk a b)) (enc nb-0 k (bltk b b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc nb m a b (bltk a b)) (enc nb-0 m a b (bltk b b)))</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 (bltk a 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-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 (bltk a b)))</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) (a a) (b b) (s b) (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 a) (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 7 (realized)</text></svg></div>

<pre>(defskeleton or
  (vars (x y mesg) (nb m nb-0 text) (a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s a) (k k))
  (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b b) (s b) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (bltk a a) (bltk a b))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 s b (bltk s b)) (1 0))
  (label 7)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((nb nb) (s a) (a a) (b b) (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>, Children: <a href="#k15">15</a> <a href="#k16">16</a>, Seen Child: <a href="#k13">13</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 (bltk s a)) (enc nb-0 k (bltk s a)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (bltk s a)) (enc nb-0 m a a (bltk s a)))</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 (bltk s a)))</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 (bltk s a)))</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 8</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 (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc nb m-0 b b (bltk s b)) (1 0))
  (label 8)
  (parent 4)
  (seen 13)
  (unrealized (1 0))
  (comment &quot;3 in cohort - 2 not yet seen&quot;))</pre>

<p id="k9">Item <a href="#t0">9</a>, Parent: <a href="#k5">5</a>, Seen Child: <a href="#k12">12</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 (bltk a b)))</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 (bltk a b)) (enc nb k (bltk b b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (bltk a b)) (enc nb m a b (bltk b b)))</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 (bltk b 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-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 (bltk b b)))</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 b))</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 b) (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 b) (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 mesg) (nb m na text) (a b name) (k skey))
  (defstrand resp 4 (x x) (y y) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s b) (k k))
  (defstrand init 1 (na na) (m m) (a a) (b b) (s b))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig (bltk a b) (bltk b b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc na m a b (bltk a b)) (1 0))
  (label 9)
  (parent 5)
  (seen 12)
  (unrealized)
  (comment &quot;1 in cohort - 0 not yet seen&quot;))</pre>

<p id="k10">Item <a href="#t0">10</a>, Parent: <a href="#k5">5</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 b x-0 (enc na m a b (bltk a b)))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat m a b 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 (bltk a b)) (enc nb k (bltk b b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (bltk a b)) (enc nb m a b (bltk b b)))</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 (bltk b 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-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 (bltk b b)))</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-0) (nb na) (m m) (a a) (b b) (s a))</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 b) (s b) (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 b) (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 10 (realized)</text></svg></div>

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

<p id="k11">Item <a href="#t0">11</a>, Parent: <a href="#k5">5</a>, Seen Child: <a href="#k13">13</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 (bltk a a)) (enc nb k (bltk a a)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (bltk a a)) (enc nb m a a (bltk a a)))</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 (bltk a a)))</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 (bltk a a)))</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 a) (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 a) (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 11 (realized)</text></svg></div>

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

<p id="k12">Item <a href="#t0">12</a>, Parent: <a href="#k6">6</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 (bltk s a)))</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 (bltk s a)) (enc nb k (bltk s b)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a b (enc na m a b (bltk s a)) (enc nb m a b (bltk s b)))</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 (bltk s 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-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 (bltk s b)))</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 12 (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 (bltk s a) (bltk s b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc na m a b (bltk s a)) (1 0))
  (label 12)
  (parent 6)
  (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="k13">Item <a href="#t0">13</a>, Parent: <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 (bltk s a)) (enc nb k (bltk s a)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (bltk s a)) (enc nb m a a (bltk s a)))</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 (bltk s a)))</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 (bltk s a)))</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 13 (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 (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc na m a a (bltk s a)) (1 0))
  (label 13)
  (parent 6)
  (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="k14">Item <a href="#t0">14</a>, Parent: <a href="#k6">6</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 (bltk s a)))</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 (bltk s a)) (enc nb k (bltk s a)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc na m a a (bltk s a)) (enc nb m a a (bltk s a)))</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 (bltk s a)))</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 (bltk s a)))</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 14 (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 (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc na m a a (bltk s a)) (1 0))
  (label 14)
  (parent 6)
  (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="k15">Item <a href="#t0">15</a>, Parent: <a href="#k8">8</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 (bltk s a)))</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 (bltk s a)) (enc nb-0 k (bltk s a)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (bltk s a)) (enc nb-0 m a a (bltk s a)))</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 (bltk s a)))</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 (bltk s a)))</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 15 (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 (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 1)
    (enc nb-0 m a a (bltk s a)) (1 0))
  (label 15)
  (parent 8)
  (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="k16">Item <a href="#t0">16</a>, Parent: <a href="#k8">8</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 (bltk s a)))</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 (bltk s a)) (enc nb-0 k (bltk s a)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat m a a (enc nb m a a (bltk s a)) (enc nb-0 m a a (bltk s a)))</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 (bltk s a)))</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 (bltk s a)))</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 16 (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 (bltk s a))
  (uniq-orig nb k)
  (operation encryption-test (added-strand resp 2)
    (enc nb-0 m a a (bltk s a)) (1 0))
  (label 16)
  (parent 8)
  (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>