station.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.6.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Station-to-station 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;Station-to-station protocol&quot; (algebra diffie-hellman))
(comment &quot;CPSA 3.6.0&quot;)
(comment &quot;All input read from station.scm&quot;)</pre>

<p id="top">Trees: <a href="#t0">0</a> <a href="#t10">10</a> <a href="#t20">20</a> <a href="#t23">23</a>.</p>

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

<div>
 <svg
  class='diagram' width='279.600pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.600 454.920' font-size='12.000'>
  <text
   x='89.880' y='401.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</text>
  <line
   x1='39.960' y1='227.460' x2='89.880' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='326.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k9&quot;, &quot;_self&quot;)'>9</text>
  <line
   x1='189.720' y1='189.960' x2='239.640' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='251.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k8&quot;, &quot;_self&quot;)'>8</text>
  <line
   x1='189.720' y1='189.960' x2='239.640' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='176.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k7&quot;, &quot;_self&quot;)'>7</text>
  <line
   x1='189.720' y1='189.960' x2='239.640' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='101.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k6&quot;, &quot;_self&quot;)'>6</text>
  <line
   x1='189.720' y1='189.960' x2='239.640' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='26.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k5&quot;, &quot;_self&quot;)'>5</text>
  <line
   x1='189.720' y1='189.960' x2='239.640' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='176.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  <line
   x1='139.800' y1='189.960' x2='189.720' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='176.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k3&quot;, &quot;_self&quot;)'>3</text>
  <line
   x1='89.880' y1='189.960' x2='139.800' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='176.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k1&quot;, &quot;_self&quot;)'>1</text>
  <line
   x1='39.960' y1='227.460' x2='89.880' y2='189.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 station-to-station diffie-hellman
  (defrole init
    (vars (x rndx) (y expt) (a b name))
    (trace (send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul x y)))))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (x expt) (a b name))
    (trace (recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul y x)))))
    (uniq-gen y)
    (absent (y (exp (gen) x)))))</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='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 (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b) (x x) (y y))</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;'>station-to-station 0</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b name) (x rndx) (y expt))
  (defstrand init 3 (a a) (b b) (x x) (y y))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (label 0)
  (unrealized (0 1))
  (origs)
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='189.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>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0))))</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>(exp (gen) x-0)</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>((a b) (b b-0) (x x) (y x-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-0) (y x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>station-to-station 1</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (x x-0) (y x))
  (defstrand init 3 (a b) (b b-0) (x x) (y x-0))
  (precedes ((0 0) (1 1)) ((1 2) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (0 1))
  (label 1)
  (parent 0)
  (unrealized (1 1))
  (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>.</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>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</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>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((b b) (y y) (x x))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((a a) (b b) (x x) (y y))</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;'>station-to-station 2 (realized)</text>
  </svg></div>

<pre>(defskeleton station-to-station
  (vars (a b name) (y x rndx))
  (defstrand init 3 (a a) (b b) (x x) (y y))
  (defstrand resp 2 (b b) (y y) (x x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (operation encryption-test (added-strand resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 2)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (y y))))
  (origs))</pre>

<p id="k3">Item <a href="#t0">3</a>, Parent: <a href="#k1">1</a>, Child: <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='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='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>(exp (gen) (mul x x-0))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: red;' 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>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 186.900 114.960 233.880 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 136.920 77.460 233.880 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a b) (b b-0) (x x) (y x-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-0) (y x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='139.920' y='39.960'
   style='text-anchor: middle;'>station-to-station 3</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (x x-0) (y x))
  (defstrand init 3 (a b) (b b-0) (x x) (y x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (precedes ((0 0) (2 0)) ((1 0) (2 0)) ((1 2) (0 1)) ((2 1) (1 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (operation encryption-test (added-listener (exp (gen) (mul x x-0)))
    (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x x-0))) (1 1))
  (label 3)
  (parent 1)
  (unrealized (2 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k4">Item <a href="#t0">4</a>, Parent: <a href="#k3">3</a>, Children: <a href="#k5">5</a> <a href="#k6">6</a> <a href="#k7">7</a> <a href="#k8">8</a> <a href="#k9">9</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) (mul x x-0 (rec w))) w)</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) (mul x x-0 (rec w))) w)</title>
   <circle style='fill: red;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 264.960 Q 192.900 264.960 145.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a b) (b b-0) (x x) (y x-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-0) (y x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 4</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 rndx) (w expt))
  (defstrand init 3 (a a) (b b) (x x-0) (y x))
  (defstrand init 3 (a b) (b b-0) (x x) (y x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) (mul x x-0 (rec w))) w))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x-0 (rec w))) w))
    (exp (gen) (mul x x-0)) (2 0))
  (label 4)
  (parent 3)
  (unrealized (3 0))
  (comment &quot;5 in cohort - 5 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (gen) (mul x x-0))</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat (gen) (mul x x-0))</title>
   <circle style='fill: red;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 264.960 Q 192.900 264.960 145.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a b) (b b-0) (x x) (y x-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-0) (y x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 5</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (x x-0) (y x))
  (defstrand init 3 (a b) (b b-0) (x x) (y x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (gen) (mul x x-0)))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x x-0)
  (precur (3 0))
  (operation nonce-test (contracted (x-1 x) (x-2 x-0) (w (mul x x-0)))
    (gen) (3 0))
  (label 5)
  (parent 4)
  (unrealized (2 0) (3 0))
  (comment &quot;empty cohort&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) x-0) x)</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) x-0) x)</title>
   <circle style='fill: red;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 264.960 Q 192.900 264.960 145.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a b) (b b-0) (x x) (y x-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-0) (y x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 6</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (x x-0) (y x))
  (defstrand init 3 (a b) (b b-0) (x x) (y x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-1) (3 0))
  (label 6)
  (parent 4)
  (unrealized (3 0))
  (comment &quot;empty cohort&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) x-0) x)</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) x-0) x)</title>
   <circle style='fill: red;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 264.960 Q 192.900 264.960 145.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a b) (b b-0) (x x-0) (y x))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x) (y x-0))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 7</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 rndx))
  (defstrand init 3 (a a) (b b) (x x) (y x-0))
  (defstrand init 3 (a b) (b b-0) (x x-0) (y x))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-0) x))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-1) (3 0))
  (label 7)
  (parent 4)
  (unrealized (3 0))
  (comment &quot;empty cohort&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='479.760pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 479.760 454.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='439.800' y1='114.960' x2='439.800' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 439.800 114.960 Q 392.820 114.960 345.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-1)</title>
   <circle cx='439.800' cy='114.960' r='6.000'/></g>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) x-1) (mul x x-0 (rec x-1)))</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) x-1) (mul x x-0 (rec x-1)))</title>
   <circle style='fill: red;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 264.960 Q 192.900 264.960 145.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x x-0))</title>
   <circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0)))</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x) (privk b-0)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x) (privk a)) (exp (gen) (mul x x-0)))</title>
   <circle cx='39.960' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x) (enc (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (exp (gen) (mul x x-0))))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((x x-1))</title>
   <text x='439.800' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a b) (b b-0) (x x) (y x-0))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-0) (y x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='239.880' y='39.960'
   style='text-anchor: middle;'>station-to-station 8</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x x-0 x-1 rndx))
  (defstrand init 3 (a a) (b b) (x x-0) (y x))
  (defstrand init 3 (a b) (b b-0) (x x) (y x-0))
  (deflistener (exp (gen) (mul x x-0)))
  (deflistener (cat (exp (gen) x-1) (mul x x-0 (rec x-1))))
  (defstrand init 1 (x x-1))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0 x-1)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (3 0))
  (label 8)
  (parent 4)
  (unrealized (2 0) (3 0))
  (comment &quot;empty cohort&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='479.760pt' height='529.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 479.760 529.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='439.800' y1='114.960' x2='439.800' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='189.960' x2='39.960' y2='489.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 439.800 189.960 Q 392.820 189.960 345.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-1)) (exp (gen) (mul x y))))</title>
   <circle cx='439.800' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='439.800' cy='114.960' r='6.000'/></g>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) y) (mul x-0 x-1 (rec y)))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) y) (mul x-0 x-1 (rec y)))</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x-0 x-1))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x-0 x-1))</title>
   <circle style='fill: red;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) x-1) (privk b)) (exp (gen) (mul x-0 x-1)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-1) (enc (enc (exp (gen) x-1) (exp (gen) x-0) (privk b-0)) (exp (gen) (mul x-0 x-1))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 189.960 Q 236.880 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-1) (exp (gen) x-0) (privk a)) (exp (gen) (mul x-0 x-1)))</title>
   <circle cx='39.960' cy='489.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) x-0) (enc (enc (exp (gen) x-0) (exp (gen) x-1) (privk b)) (exp (gen) (mul x-0 x-1))))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-1)</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>((b b-1) (y y) (x x))</title>
   <text x='439.800' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((a b) (b b-0) (x x-0) (y x-1))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (x x-1) (y x-0))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='239.880' y='39.960'
   style='text-anchor: middle;'>station-to-station 9</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (x expt) (x-0 x-1 y rndx))
  (defstrand init 3 (a a) (b b) (x x-1) (y x-0))
  (defstrand init 3 (a b) (b b-0) (x x-0) (y x-1))
  (deflistener (exp (gen) (mul x-0 x-1)))
  (deflistener (cat (exp (gen) y) (mul x-0 x-1 (rec y))))
  (defstrand resp 2 (b b-1) (y y) (x x))
  (precedes ((0 0) (3 0)) ((1 0) (3 0)) ((1 2) (0 1)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x-0 x-1 y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (3 0))
  (label 9)
  (parent 4)
  (unrealized (2 0) (3 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="t10">Tree <a href="#top">10</a>.</p>

<div>
 <svg
  class='diagram' width='279.600pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.600 454.920' font-size='12.000'>
  <text
   x='239.640' y='401.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k19&quot;, &quot;_self&quot;)'>19</text>
  <line
   x1='189.720' y1='264.960' x2='239.640' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='326.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k18&quot;, &quot;_self&quot;)'>18</text>
  <line
   x1='189.720' y1='264.960' x2='239.640' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='251.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k17&quot;, &quot;_self&quot;)'>17</text>
  <line
   x1='189.720' y1='264.960' x2='239.640' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='176.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k16&quot;, &quot;_self&quot;)'>16</text>
  <line
   x1='189.720' y1='264.960' x2='239.640' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='239.640' y='101.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k15&quot;, &quot;_self&quot;)'>15</text>
  <line
   x1='189.720' y1='264.960' x2='239.640' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='251.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k14&quot;, &quot;_self&quot;)'>14</text>
  <line
   x1='139.800' y1='264.960' x2='189.720' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='251.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k13&quot;, &quot;_self&quot;)'>13</text>
  <line
   x1='89.880' y1='227.460' x2='139.800' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k12&quot;, &quot;_self&quot;)'>12</text>
  <line
   x1='89.880' y1='227.460' x2='139.800' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='213.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k11&quot;, &quot;_self&quot;)'>11</text>
  <line
   x1='39.960' y1='227.460' x2='89.880' y2='227.460'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='213.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k10&quot;, &quot;_self&quot;)'>10</text>
  </svg></div>

<pre>(defprotocol station-to-station diffie-hellman
  (defrole init
    (vars (x rndx) (y expt) (a b name))
    (trace (send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul x y)))))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (x expt) (a b name))
    (trace (recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul y x)))))
    (uniq-gen y)
    (absent (y (exp (gen) x)))))</pre>

<p id="k10">Item <a href="#t10">10</a>, Child: <a href="#k11">11</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 (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b) (y y) (x x))</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;'>station-to-station 10</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b name) (y rndx) (x expt))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (label 10)
  (unrealized (0 2))
  (origs)
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k11">Item <a href="#t10">11</a>, Parent: <a href="#k10">10</a>, Children: <a href="#k12">12</a> <a href="#k13">13</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</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 (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</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;'>station-to-station 11</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation encryption-test (added-strand init 3)
    (enc (exp (gen) x) (exp (gen) y) (privk a)) (0 2))
  (label 11)
  (parent 10)
  (unrealized (1 1))
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k12">Item <a href="#t10">12</a>, Parent: <a href="#k11">11</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</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>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</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;'>station-to-station 12 (realized)</text>
  </svg></div>

<pre>(defskeleton station-to-station
  (vars (a b name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b) (x x) (y y))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul y x))) (1 1))
  (label 12)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (x x))))
  (origs))</pre>

<p id="k13">Item <a href="#t10">13</a>, Parent: <a href="#k11">11</a>, Child: <a href="#k14">14</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='189.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 264.960 Q 192.900 264.960 145.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x y))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x y))</title>
   <circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
  <path
   d='M 139.920 339.960 Q 92.940 339.960 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 136.920 152.460 233.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</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;'>station-to-station 13</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation encryption-test (added-listener (exp (gen) (mul x y)))
    (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
      (exp (gen) (mul x y))) (1 1))
  (label 13)
  (parent 11)
  (unrealized (2 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k14">Item <a href="#t10">14</a>, Parent: <a href="#k13">13</a>, Children: <a href="#k15">15</a> <a href="#k16">16</a> <a href="#k17">17</a> <a href="#k18">18</a> <a href="#k19">19</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) (mul x y (rec w))) w)</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) (mul x y (rec w))) w)</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x y))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x y))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 14</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x y rndx) (w expt))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) (mul x y (rec w))) w))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x y (rec w))) w))
    (exp (gen) (mul x y)) (2 0))
  (label 14)
  (parent 13)
  (unrealized (3 0))
  (comment &quot;5 in cohort - 5 not yet seen&quot;))</pre>

<p id="k15">Item <a href="#t10">15</a>, Parent: <a href="#k14">14</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (gen) (mul x y))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (gen) (mul x y))</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x y))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x y))</title>
   <circle style='fill: red;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 15</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (3 0))
  (operation nonce-test (contracted (x-0 x) (y-0 y) (w (mul x y))) (gen)
    (3 0))
  (label 15)
  (parent 14)
  (unrealized (2 0) (3 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="k16">Item <a href="#t10">16</a>, Parent: <a href="#k14">14</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) x) y)</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) x) y)</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul y x))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul y x))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul y x))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 16</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (y x rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-0) (3 0))
  (label 16)
  (parent 14)
  (unrealized (3 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="k17">Item <a href="#t10">17</a>, Parent: <a href="#k14">14</a>.</p>

<div>
 <svg
  class='diagram' width='479.760pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 479.760 454.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='439.800' y1='114.960' x2='439.800' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 439.800 114.960 Q 392.220 150.660 344.639 186.359'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='439.800' cy='114.960' r='6.000'/></g>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) x-0) (mul x y (rec x-0)))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) x-0) (mul x y (rec x-0)))</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x y))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x y))</title>
   <circle style='fill: red;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((x x-0))</title>
   <text x='439.800' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='239.880' y='39.960'
   style='text-anchor: middle;'>station-to-station 17</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x y x-0 rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x y (rec x-0))))
  (defstrand init 1 (x x-0))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (3 0))
  (label 17)
  (parent 14)
  (unrealized (2 0) (3 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="k18">Item <a href="#t10">18</a>, Parent: <a href="#k14">14</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.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='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) y) x)</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) y) x)</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x y))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x y))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>station-to-station 18</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 name) (x y rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x))
  (defstrand init 3 (a a) (b b-0) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y)
  (operation nonce-test (displaced 4 0 resp 2) (exp (gen) y-0) (3 0))
  (label 18)
  (parent 14)
  (unrealized (3 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="k19">Item <a href="#t10">19</a>, Parent: <a href="#k14">14</a>.</p>

<div>
 <svg
  class='diagram' width='479.760pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 479.760 454.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='439.800' y1='114.960' x2='439.800' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='264.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 439.800 189.960 Q 392.820 189.960 345.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y-0) (enc (enc (exp (gen) y-0) (exp (gen) x) (privk b-1)) (exp (gen) (mul x y-0))))</title>
   <circle cx='439.800' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='439.800' cy='114.960' r='6.000'/></g>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (exp (gen) y-0) (mul x-0 y (rec y-0)))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat (exp (gen) y-0) (mul x-0 y (rec y-0)))</title>
   <circle style='fill: red;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) (mul x-0 y))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(exp (gen) (mul x-0 y))</title>
   <circle style='fill: red;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) y) (privk a)) (exp (gen) (mul x-0 y)))</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x-0) (privk b-0)) (exp (gen) (mul x-0 y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <path
   d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(exp (gen) x-0)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x-0) (exp (gen) y) (privk a)) (exp (gen) (mul x-0 y)))</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x-0) (privk b)) (exp (gen) (mul x-0 y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x-0)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((b b-1) (y y-0) (x x))</title>
   <text x='439.800' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((a a) (b b-0) (x x-0) (y y))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x-0))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='239.880' y='39.960'
   style='text-anchor: middle;'>station-to-station 19</text></svg></div>

<pre>(defskeleton station-to-station
  (vars (a b b-0 b-1 name) (x expt) (x-0 y y-0 rndx))
  (defstrand resp 3 (a a) (b b) (y y) (x x-0))
  (defstrand init 3 (a a) (b b-0) (x x-0) (y y))
  (deflistener (exp (gen) (mul x-0 y)))
  (deflistener (cat (exp (gen) y-0) (mul x-0 y (rec y-0))))
  (defstrand resp 2 (b b-1) (y y-0) (x x))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x-0 y y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (label 19)
  (parent 14)
  (unrealized (2 0) (3 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="t20">Tree <a href="#top">20</a>.</p>

<div>
 <svg
  class='diagram' width='129.840pt' height='154.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 129.840 154.920' font-size='12.000'>
  <text
   x='89.880' y='101.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k22&quot;, &quot;_self&quot;)'>22</text>
  <line
   x1='39.960' y1='77.460' x2='89.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k21&quot;, &quot;_self&quot;)'>21</text>
  <line
   x1='39.960' y1='77.460' x2='89.880' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='63.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k20&quot;, &quot;_self&quot;)'>20</text>
  </svg></div>

<pre>(defprotocol station-weak diffie-hellman
  (defrole weak-init
    (vars (x rndx) (y expt) (a b name))
    (trace (send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul x y))))))
  (defrole weak-resp
    (vars (y rndx) (x expt) (a b name))
    (trace (recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul y x)))))
    (absent (y (exp (gen) x)))))</pre>

<p id="k20">Item <a href="#t20">20</a>, Children: <a href="#k21">21</a> <a href="#k22">22</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 (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b) (x x) (y y))</title>
   <text
    x='39.960' y='77.460' style='text-anchor: middle;'>weak-init</text>
   </g>
  <text
   x='39.960' y='39.960'
   style='text-anchor: middle;'>station-weak 20</text></svg></div>

<pre>(defskeleton station-weak
  (vars (a b name) (x rndx) (y expt))
  (defstrand weak-init 3 (a a) (b b) (x x) (y y))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (label 20)
  (unrealized (0 1))
  (origs)
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k21">Item <a href="#t20">21</a>, Parent: <a href="#k20">20</a>.</p>

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

<pre>(defskeleton station-weak
  (vars (a b b-0 name) (x x-0 rndx))
  (defstrand weak-init 3 (a a) (b b) (x x-0) (y x))
  (defstrand weak-init 3 (a b) (b b-0) (x x) (y x-0))
  (precedes ((0 0) (1 1)) ((1 2) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x-0)
  (operation encryption-test (added-strand weak-init 3)
    (enc (exp (gen) x) (exp (gen) x-0) (privk b)) (0 1))
  (label 21)
  (parent 20)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x-0) (y x))))
  (origs))</pre>

<p id="k22">Item <a href="#t20">22</a>, Parent: <a href="#k20">20</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>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</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>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((b b) (y y) (x x))</title>
   <text
    x='139.920' y='77.460' style='text-anchor: middle;'>weak-resp</text>
   </g>
  <g><title>((a a) (b b) (x x) (y y))</title>
   <text
    x='39.960' y='77.460' style='text-anchor: middle;'>weak-init</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>station-weak 22 (realized)</text></svg>
 </div>

<pre>(defskeleton station-weak
  (vars (a b name) (y x rndx))
  (defstrand weak-init 3 (a a) (b b) (x x) (y y))
  (defstrand weak-resp 2 (b b) (y y) (x x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
  (label 22)
  (parent 20)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (y y))))
  (origs))</pre>

<p id="t23">Tree <a href="#top">23</a>.</p>

<div>
 <svg
  class='diagram' width='129.840pt' height='154.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 129.840 154.920' font-size='12.000'>
  <text
   x='89.880' y='101.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k25&quot;, &quot;_self&quot;)'>25</text>
  <line
   x1='39.960' y1='77.460' x2='89.880' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k24&quot;, &quot;_self&quot;)'>24</text>
  <line
   x1='39.960' y1='77.460' x2='89.880' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='63.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k23&quot;, &quot;_self&quot;)'>23</text>
  </svg></div>

<pre>(defprotocol station-weak diffie-hellman
  (defrole weak-init
    (vars (x rndx) (y expt) (a b name))
    (trace (send (exp (gen) x))
      (recv
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul x y)))))
      (send
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul x y))))))
  (defrole weak-resp
    (vars (y rndx) (x expt) (a b name))
    (trace (recv (exp (gen) x))
      (send
        (cat (exp (gen) y)
          (enc (enc (exp (gen) y) (exp (gen) x) (privk b))
            (exp (gen) (mul y x)))))
      (recv
        (enc (enc (exp (gen) x) (exp (gen) y) (privk a))
          (exp (gen) (mul y x)))))
    (absent (y (exp (gen) x)))))</pre>

<p id="k23">Item <a href="#t23">23</a>, Children: <a href="#k24">24</a> <a href="#k25">25</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 (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul y x)))</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul y x))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text
    x='39.960' y='77.460' style='text-anchor: middle;'>weak-resp</text>
   </g>
  <text
   x='39.960' y='39.960'
   style='text-anchor: middle;'>station-weak 23</text></svg></div>

<pre>(defskeleton station-weak
  (vars (a b name) (y rndx) (x expt))
  (defstrand weak-resp 3 (a a) (b b) (y y) (x x))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (label 23)
  (unrealized (0 2))
  (origs)
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k24">Item <a href="#t23">24</a>, Parent: <a href="#k23">23</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g>
   <title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b-0)) (exp (gen) (mul x y))))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='139.920' cy='114.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</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 (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((a a) (b b-0) (x x) (y y))</title>
   <text
    x='139.920' y='77.460' style='text-anchor: middle;'>weak-init</text>
   </g>
  <g><title>((a a) (b b) (y y) (x x))</title>
   <text
    x='39.960' y='77.460' style='text-anchor: middle;'>weak-resp</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>station-weak 24 (realized)</text></svg>
 </div>

<pre>(defskeleton station-weak
  (vars (a b b-0 name) (x y rndx))
  (defstrand weak-resp 3 (a a) (b b) (y y) (x x))
  (defstrand weak-init 3 (a a) (b b-0) (x x) (y y))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (operation encryption-test (added-strand weak-init 3)
    (enc (exp (gen) x) (exp (gen) y) (privk a)) (0 2))
  (label 24)
  (parent 23)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (x x))))
  (origs))</pre>

<p id="k25">Item <a href="#t23">25</a>, Parent: <a href="#k23">23</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='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='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>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) y-0) (privk a)) (exp (gen) (mul y y-0))))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) y-0)</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g>
   <title>(enc (enc (exp (gen) y) (exp (gen) y-0) (privk a)) (exp (gen) (mul y y-0)))</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 (exp (gen) y-0) (enc (enc (exp (gen) y-0) (exp (gen) y) (privk b)) (exp (gen) (mul y y-0))))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) y)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((b a) (y y) (x y-0))</title>
   <text
    x='139.920' y='77.460' style='text-anchor: middle;'>weak-resp</text>
   </g>
  <g><title>((a a) (b b) (y y-0) (x y))</title>
   <text
    x='39.960' y='77.460' style='text-anchor: middle;'>weak-resp</text>
   </g>
  <text
   x='89.940' y='39.960'
   style='text-anchor: middle;'>station-weak 25 (realized)</text></svg>
 </div>

<pre>(defskeleton station-weak
  (vars (a b name) (y y-0 rndx))
  (defstrand weak-resp 3 (a a) (b b) (y y-0) (x y))
  (defstrand weak-resp 2 (b a) (y y) (x y-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y (exp (gen) y-0)) (y-0 (exp (gen) y)))
  (non-orig (privk a) (privk b))
  (uniq-gen y-0)
  (operation encryption-test (added-strand weak-resp 2)
    (enc (exp (gen) y) (exp (gen) y-0) (privk a)) (0 2))
  (label 25)
  (parent 23)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (y y-0) (x y))))
  (origs))</pre>

</body>
</html>