cpsa-3.3.0: doc/examples/station.xhtml
<?xml version="1.0"?>
<!-- CPSA 3.2.2 -->
<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 "Station-to-station protocol" (algebra diffie-hellman))
(comment "CPSA 3.2.2")
(comment "All input read from station_to_station.scm")</pre>
<p id="top">Trees: <a href="#t0">0</a> <a href="#t9">9</a>.</p>
<p id="t0">Tree <a href="#top">0</a>.</p>
<div>
<svg
class='diagram' width='279.600pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.600 304.920' font-size='12.000'>
<text
x='189.720' y='251.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k7", "_self")'>7</text>
<line
x1='139.800' y1='227.460' x2='189.720' 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("#k8", "_self")'>8</text>
<line
x1='189.720' y1='189.960' x2='239.640' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='176.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k6", "_self")'>6</text>
<line
x1='139.800' y1='227.460' x2='189.720' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='213.540' style='text-anchor: middle; fill: red;'
onclick='window.open("#k5", "_self")'>5</text>
<line
x1='89.880' y1='227.460' x2='139.800' y2='227.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='213.540' style='text-anchor: middle; fill: red;'
onclick='window.open("#k3", "_self")'>3</text>
<line
x1='39.960' y1='152.460' x2='89.880' y2='227.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='101.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k2", "_self")'>2</text>
<line
x1='39.960' y1='152.460' x2='89.880' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='26.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k4", "_self")'>4</text>
<line
x1='89.880' y1='39.960' x2='139.800' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='26.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k1", "_self")'>1</text>
<line
x1='39.960' y1='152.460' x2='89.880' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='138.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k0", "_self")'>0</text>
</svg></div>
<pre>(defprotocol station-to-station diffie-hellman
(defrole init
(vars (x expn) (h base) (a b name))
(trace (send (exp (gen) x))
(recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
(send (enc (enc (exp (gen) x) h (privk a)) (exp h x))))
(uniq-gen x))
(defrole resp
(vars (y expn) (h base) (a b name))
(trace (recv h)
(send
(cat (exp (gen) y)
(enc (enc (exp (gen) y) h (privk b)) (exp h y))))
(recv (enc (enc h (exp (gen) y) (privk a)) (exp h y))))
(uniq-gen y)
(ind-zero-in (y h))))</pre>
<p id="k0">Item <a href="#t0">0</a>, Children: <a href="#k1">1</a> <a href="#k2">2</a> <a href="#k3">3</a>.</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) h (privk a)) (exp h x))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g>
<title>(cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x)))</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) (h h) (x x))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text
x='39.960' y='39.960'
style='text-anchor: middle;'>station-to-station 0</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (h base) (x expn))
(defstrand init 3 (a a) (b b) (h h) (x x))
(non-orig (privk a) (privk b))
(uniq-gen x)
(label 0)
(unrealized (0 1))
(origs)
(comment "3 in cohort - 3 not yet seen"))</pre>
<p id="k1">Item <a href="#t0">1</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k4">4</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='379.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 379.920' font-size='12.000'>
<defs>
<marker
id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
refY='5'>
<path
d='M 0 0 5 5 0 10'
style='stroke-width: 2; fill: none; stroke: black;'/></marker>
</defs>
<line
x1='139.920' y1='114.960' x2='139.920' y2='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-0) (exp (gen) x) (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) (enc (enc (exp (gen) x) (exp (gen) x-0) (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-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='339.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='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)</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((a b) (b b-0) (h (exp (gen) x)) (x x-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x-0)) (x x))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>station-to-station 1</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (x x-0 expn))
(defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
(defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x 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 (enc (exp (gen) x-0) (exp (gen) x) (privk b))
(exp (gen) (mul x x-0))) (0 1))
(label 1)
(parent 0)
(unrealized (1 1))
(comment "1 in cohort - 1 not yet seen"))</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 x y))))</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 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: 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) (h (exp (gen) x)) (y y))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) y)) (x x))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>station-to-station 2 (realized)</text>
</svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (x y expn))
(defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
(defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen x y)
(operation encryption-test (added-strand resp 2)
(enc (enc (exp (gen) y) (exp (gen) x) (privk b))
(exp (gen) (mul x y))) (0 1))
(label 2)
(parent 0)
(unrealized)
(shape)
(maps ((0) ((a a) (b b) (x x) (h (exp (gen) y)))))
(origs))</pre>
<p id="k3">Item <a href="#t0">3</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k5">5</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 304.920' font-size='12.000'>
<defs>
<marker
id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
refY='5'>
<path
d='M 0 0 5 5 0 10'
style='stroke-width: 2; fill: none; stroke: black;'/></marker>
</defs>
<line
x1='139.920' y1='114.960' x2='139.920' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 139.920 189.960 Q 92.940 189.960 45.960 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp h x)</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(exp h x)</title>
<circle style='fill: red;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc (enc (exp (gen) x) h (privk a)) (exp h x))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g>
<title>(cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x)))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) x)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((a a) (b b) (h h) (x x))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>station-to-station 3</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (h base) (x expn))
(defstrand init 3 (a a) (b b) (h h) (x x))
(deflistener (exp h x))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-gen x)
(operation encryption-test (added-listener (exp h x))
(enc (enc h (exp (gen) x) (privk b)) (exp h x)) (0 1))
(label 3)
(parent 0)
(unrealized (0 1) (1 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k4">Item <a href="#t0">4</a>, Parent: <a href="#k1">1</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-0) (exp (gen) x) (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) (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='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-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='339.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='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)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((a b) (b b-0) (h (exp (gen) x)) (x x-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x-0)) (x 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 4</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (x x-0 expn))
(defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
(defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x 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) (exp (gen) x-0) (privk b-0))
(exp (gen) (mul x x-0))) (1 1))
(label 4)
(parent 1)
(unrealized (2 0))
(comment "empty cohort"))</pre>
<p id="k5">Item <a href="#t0">5</a>, Parent: <a href="#k3">3</a>, Children: <a href="#k6">6</a> <a href="#k7">7</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 304.920' font-size='12.000'>
<defs>
<marker
id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
refY='5'>
<path
d='M 0 0 5 5 0 10'
style='stroke-width: 2; fill: none; stroke: black;'/></marker>
</defs>
<line
x1='139.920' y1='114.960' x2='139.920' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 139.920 189.960 Q 92.940 189.960 45.960 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) (mul x x-0))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(exp (gen) (mul x x-0))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(enc (enc (exp (gen) x) (exp (gen) x-0) (privk a)) (exp (gen) (mul x x-0)))</title>
<circle cx='39.960' 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)) (exp (gen) (mul x x-0))))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) x)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((a a) (b b) (h (exp (gen) x-0)) (x x))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>station-to-station 5</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (x expn) (x-0 expr))
(defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
(deflistener (exp (gen) (mul x x-0)))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-gen x)
(operation nonce-test (algebra-contracted (h (exp (gen) x-0)))
(exp (gen) (mul x x-0)) (1 0) (exp (gen) x))
(label 5)
(parent 3)
(unrealized (0 1))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k6">Item <a href="#t0">6</a>, Parent: <a href="#k5">5</a>, Child: <a href="#k8">8</a>.</p>
<div>
<svg
class='diagram' width='279.840pt' height='379.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.840 379.920' font-size='12.000'>
<defs>
<marker
id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
refY='5'>
<path
d='M 0 0 5 5 0 10'
style='stroke-width: 2; fill: none; stroke: black;'/></marker>
</defs>
<line
x1='239.880' y1='114.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='114.960' x2='139.920' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='339.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 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-0) (exp (gen) x) (privk b)) (exp (gen) (mul x x-0)))</title>
<circle cx='239.880' cy='264.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: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<path
d='M 239.880 114.960 Q 192.900 114.960 145.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) x-0)</title>
<circle cx='239.880' cy='114.960' r='6.000'/></g>
<path
d='M 139.920 189.960 Q 92.340 225.660 44.759 261.359'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) (mul x x-0))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(exp (gen) (mul x x-0))</title>
<circle style='fill: red;' 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='339.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='264.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 39.960 114.960 Q 137.111 113.906 234.262 187.853'
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) (h (exp (gen) x)) (x x-0))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x-0)) (x 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 6</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (x x-0 expn))
(defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
(deflistener (exp (gen) (mul x x-0)))
(defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
(precedes ((0 0) (1 0)) ((0 0) (2 1)) ((1 1) (0 1)) ((2 0) (1 0))
((2 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-0) (exp (gen) x) (privk b)) (0 1))
(label 6)
(parent 5)
(unrealized (1 0) (2 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k7">Item <a href="#t0">7</a>, Parent: <a href="#k5">5</a>.</p>
<div>
<svg
class='diagram' width='279.840pt' height='379.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.840 379.920' font-size='12.000'>
<defs>
<marker
id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
refY='5'>
<path
d='M 0 0 5 5 0 10'
style='stroke-width: 2; fill: none; stroke: black;'/></marker>
</defs>
<line
x1='239.880' y1='114.960' x2='239.880' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='189.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='339.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (exp (gen) y) (enc (enc (exp (gen) y) (exp (gen) x) (privk b)) (exp (gen) (mul x y))))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(exp (gen) x)</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<path
d='M 139.920 264.960 Q 92.940 264.960 45.960 264.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) (mul x y))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul x y))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g>
<title>(enc (enc (exp (gen) x) (exp (gen) y) (privk a)) (exp (gen) (mul x y)))</title>
<circle cx='39.960' cy='339.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: 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-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) (h (exp (gen) x)) (y y))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) y)) (x 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 7</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (x y expn))
(defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
(deflistener (exp (gen) (mul x y)))
(defstrand resp 2 (b b) (h (exp (gen) x)) (y y))
(precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen x y)
(operation encryption-test (added-strand resp 2)
(enc (exp (gen) y) (exp (gen) x) (privk b)) (0 1))
(label 7)
(parent 5)
(unrealized (1 0))
(comment "empty cohort"))</pre>
<p id="k8">Item <a href="#t0">8</a>, Parent: <a href="#k6">6</a>.</p>
<div>
<svg
class='diagram' width='379.800pt' height='379.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.800 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='339.840' y1='114.960' x2='339.840' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='239.880' y1='114.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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='339.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 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>(exp (gen) (mul x x-0))</title>
<circle cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(exp (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 142.920 227.460 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-0) (exp (gen) x) (privk b)) (exp (gen) (mul x x-0)))</title>
<circle cx='239.880' cy='264.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='239.880' cy='189.960' r='6.000'/></g>
<path
d='M 239.880 114.960 Q 192.900 114.960 145.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 239.880 114.960 Q 286.860 114.960 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='239.880' cy='114.960' r='6.000'/></g>
<path
d='M 139.920 189.960 Q 92.340 225.660 44.759 261.359'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(exp (gen) (mul x x-0))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(exp (gen) (mul x x-0))</title>
<circle style='fill: red;' 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='339.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='264.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<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) (h (exp (gen) x)) (x x-0))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x-0)) (x 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 8</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (x x-0 expn))
(defstrand init 3 (a a) (b b) (h (exp (gen) x-0)) (x x))
(deflistener (exp (gen) (mul x x-0)))
(defstrand init 3 (a b) (b b-0) (h (exp (gen) x)) (x x-0))
(deflistener (exp (gen) (mul x x-0)))
(precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 0) (1 0))
((2 0) (3 0)) ((2 2) (0 1)) ((3 1) (2 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) (exp (gen) x-0) (privk b-0))
(exp (gen) (mul x x-0))) (2 1))
(label 8)
(parent 6)
(unrealized (1 0) (3 0))
(comment "empty cohort"))</pre>
<p id="t9">Tree <a href="#top">9</a>.</p>
<div>
<svg
class='diagram' width='279.600pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.600 304.920' font-size='12.000'>
<text
x='239.640' y='251.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k17", "_self")'>17</text>
<line
x1='189.720' y1='227.460' 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("#k16", "_self")'>16</text>
<line
x1='189.720' y1='227.460' x2='239.640' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='213.540' style='text-anchor: middle; fill: red;'
onclick='window.open("#k15", "_self")'>15</text>
<line
x1='139.800' y1='227.460' x2='189.720' y2='227.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='213.540' style='text-anchor: middle; fill: red;'
onclick='window.open("#k14", "_self")'>14</text>
<line
x1='89.880' y1='227.460' x2='139.800' y2='227.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='213.540' style='text-anchor: middle; fill: red;'
onclick='window.open("#k11", "_self")'>11</text>
<line
x1='39.960' y1='152.460' x2='89.880' y2='227.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='101.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k13", "_self")'>13</text>
<line
x1='89.880' y1='77.460' x2='139.800' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k12", "_self")'>12</text>
<line
x1='89.880' y1='77.460' x2='139.800' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='63.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k10", "_self")'>10</text>
<line
x1='39.960' y1='152.460' x2='89.880' y2='77.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='138.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k9", "_self")'>9</text>
</svg></div>
<pre>(defprotocol station-to-station diffie-hellman
(defrole init
(vars (x expn) (h base) (a b name))
(trace (send (exp (gen) x))
(recv (cat h (enc (enc h (exp (gen) x) (privk b)) (exp h x))))
(send (enc (enc (exp (gen) x) h (privk a)) (exp h x))))
(uniq-gen x))
(defrole resp
(vars (y expn) (h base) (a b name))
(trace (recv h)
(send
(cat (exp (gen) y)
(enc (enc (exp (gen) y) h (privk b)) (exp h y))))
(recv (enc (enc h (exp (gen) y) (privk a)) (exp h y))))
(uniq-gen y)
(ind-zero-in (y h))))</pre>
<p id="k9">Item <a href="#t9">9</a>, Children: <a href="#k10">10</a> <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 h (exp (gen) y) (privk a)) (exp h y))</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) h (privk b)) (exp h y)))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>h</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((a a) (b b) (h h) (y y))</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 9</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (h base) (y expn))
(defstrand resp 3 (a a) (b b) (h h) (y y))
(ind-zero-in (y h))
(non-orig (privk a) (privk b))
(uniq-gen y)
(label 9)
(unrealized (0 2))
(origs)
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k10">Item <a href="#t9">10</a>, Parent: <a href="#k9">9</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 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-0)) (exp (gen) (mul y x))))</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 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-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) (h (exp (gen) y)) (x x))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x)) (y y))</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 10</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (y x expn))
(defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
(defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
(precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen y x)
(operation encryption-test (added-strand init 3)
(enc (enc (exp (gen) x) (exp (gen) y) (privk a))
(exp (gen) (mul y x))) (0 2))
(label 10)
(parent 9)
(unrealized (1 1))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k11">Item <a href="#t9">11</a>, Parent: <a href="#k9">9</a>, Child: <a href="#k14">14</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>(exp h y)</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(exp h y)</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc (enc h (exp (gen) y) (privk a)) (exp h y))</title>
<circle style='fill: red;' 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) h (privk b)) (exp h y)))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>h</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((a a) (b b) (h h) (y y))</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 name) (h base) (y expn))
(defstrand resp 3 (a a) (b b) (h h) (y y))
(deflistener (exp h y))
(precedes ((0 1) (1 0)) ((1 1) (0 2)))
(ind-zero-in (y h))
(non-orig (privk a) (privk b))
(uniq-gen y)
(operation encryption-test (added-listener (exp h y))
(enc (enc h (exp (gen) y) (privk a)) (exp h y)) (0 2))
(label 11)
(parent 9)
(unrealized (0 2) (1 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k12">Item <a href="#t9">12</a>, Parent: <a href="#k10">10</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)) (exp (gen) (mul x y))))</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 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-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) (h (exp (gen) y)) (x x))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x)) (y y))</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) (x y expn))
(defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
(defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
(precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen x y)
(operation encryption-test (displaced 2 0 resp 2)
(enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
(exp (gen) (mul x y))) (1 1))
(label 12)
(parent 10)
(unrealized)
(shape)
(maps ((0) ((a a) (b b) (y y) (h (exp (gen) x)))))
(origs))</pre>
<p id="k13">Item <a href="#t9">13</a>, Parent: <a href="#k10">10</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 y x))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul y x))</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 y x)))</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 y x))))</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 y x)))</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 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) (h (exp (gen) y)) (x x))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x)) (y y))</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) (y x expn))
(defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
(defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
(deflistener (exp (gen) (mul y x)))
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2)) ((2 1) (1 1)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen y x)
(operation encryption-test (added-listener (exp (gen) (mul y x)))
(enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
(exp (gen) (mul y x))) (1 1))
(label 13)
(parent 10)
(unrealized (2 0))
(comment "empty cohort"))</pre>
<p id="k14">Item <a href="#t9">14</a>, Parent: <a href="#k11">11</a>, Child: <a href="#k15">15</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>(exp (gen) (mul y y-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul y y-0))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g>
<title>(enc (enc (exp (gen) y-0) (exp (gen) y) (privk a)) (exp (gen) (mul y y-0)))</title>
<circle style='fill: red;' 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) y-0) (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-0)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((a a) (b b) (h (exp (gen) y-0)) (y y))</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 14</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (y expn) (y-0 expr))
(defstrand resp 3 (a a) (b b) (h (exp (gen) y-0)) (y y))
(deflistener (exp (gen) (mul y y-0)))
(precedes ((0 1) (1 0)) ((1 1) (0 2)))
(ind-zero-in (y (exp (gen) y-0)))
(non-orig (privk a) (privk b))
(uniq-gen y)
(operation nonce-test (algebra-contracted (h (exp (gen) y-0)))
(exp (gen) (mul y y-0)) (1 0) (exp (gen) y)
(enc (enc (exp (gen) y) (exp (gen) y-0) (privk b))
(exp (gen) (mul y y-0))))
(label 14)
(parent 11)
(unrealized (0 2))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k15">Item <a href="#t9">15</a>, Parent: <a href="#k14">14</a>, Children: <a href="#k16">16</a> <a href="#k17">17</a>.</p>
<div>
<svg
class='diagram' width='279.840pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.840 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='239.880' y1='114.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='189.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 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='239.880' 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 y x))))</title>
<circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<path
d='M 239.880 114.960 Q 142.920 77.460 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='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>(exp (gen) (mul y x))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul y x))</title>
<circle style='fill: red;' cx='139.920' cy='189.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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<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 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) (h (exp (gen) y)) (x x))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x)) (y y))</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 15</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (y x expn))
(defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
(deflistener (exp (gen) (mul y x)))
(defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
(precedes ((0 1) (1 0)) ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0))
((2 2) (0 2)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen y x)
(operation encryption-test (added-strand init 3)
(enc (exp (gen) x) (exp (gen) y) (privk a)) (0 2))
(label 15)
(parent 14)
(unrealized (1 0) (2 1))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k16">Item <a href="#t9">16</a>, Parent: <a href="#k15">15</a>.</p>
<div>
<svg
class='diagram' width='279.840pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.840 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='239.880' y1='114.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='189.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 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='239.880' 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: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
<path
d='M 239.880 114.960 Q 142.920 77.460 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='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>(exp (gen) (mul x y))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul x y))</title>
<circle style='fill: red;' cx='139.920' cy='189.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;'/>
<path
d='M 39.960 189.960 Q 136.920 152.460 233.880 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 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) (h (exp (gen) y)) (x x))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x)) (y y))</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 16</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b name) (x y expn))
(defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
(deflistener (exp (gen) (mul x y)))
(defstrand init 3 (a a) (b b) (h (exp (gen) y)) (x x))
(precedes ((0 1) (1 0)) ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0))
((2 2) (0 2)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen x y)
(operation encryption-test (displaced 3 0 resp 2)
(enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
(exp (gen) (mul x y))) (2 1))
(label 16)
(parent 15)
(unrealized (1 0))
(comment "empty cohort"))</pre>
<p id="k17">Item <a href="#t9">17</a>, Parent: <a href="#k15">15</a>.</p>
<div>
<svg
class='diagram' width='379.800pt' height='379.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.800 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='339.840' y1='189.960' x2='339.840' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='239.880' y1='114.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='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 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>(exp (gen) (mul y x))</title>
<circle cx='339.840' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul 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 142.920 302.460 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 y x)))</title>
<circle cx='239.880' 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 y x))))</title>
<circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
<path
d='M 239.880 114.960 Q 142.920 77.460 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='239.880' cy='114.960' r='6.000'/></g>
<path
d='M 139.920 264.960 Q 92.340 300.660 44.759 336.359'
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='139.920' cy='264.960' r='6.000'/></g>
<g><title>(exp (gen) (mul y x))</title>
<circle style='fill: red;' cx='139.920' cy='189.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='339.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;'/>
<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) (h (exp (gen) y)) (x x))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((a a) (b b) (h (exp (gen) x)) (y y))</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 17</text></svg></div>
<pre>(defskeleton station-to-station
(vars (a b b-0 name) (y x expn))
(defstrand resp 3 (a a) (b b) (h (exp (gen) x)) (y y))
(deflistener (exp (gen) (mul y x)))
(defstrand init 3 (a a) (b b-0) (h (exp (gen) y)) (x x))
(deflistener (exp (gen) (mul y x)))
(precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 0) (0 0))
((2 2) (0 2)) ((3 1) (2 1)))
(ind-zero-in (y (exp (gen) x)))
(non-orig (privk a) (privk b))
(uniq-gen y x)
(operation encryption-test (added-listener (exp (gen) (mul y x)))
(enc (enc (exp (gen) y) (exp (gen) x) (privk b-0))
(exp (gen) (mul y x))) (2 1))
(label 17)
(parent 15)
(unrealized (1 0) (3 0))
(comment "empty cohort"))</pre>
</body>
</html>