cpsa-3.6.0: doc/examples/woolam.xhtml
<?xml version="1.0"?>
<!-- CPSA 3.6.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Woo-Lam 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 "Woo-Lam Protocol")
(comment "CPSA 3.6.0")
(comment "All input read from woolam.scm")</pre>
<p id="t0">Tree 0.</p>
<div>
<svg
class='diagram' width='229.680pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 229.680 79.920' font-size='12.000'>
<text
x='189.720' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k3", "_self")'>3</text>
<line
x1='139.800' y1='39.960' x2='189.720' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='26.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k2", "_self")'>2</text>
<line
x1='89.880' y1='39.960' x2='139.800' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='26.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k1", "_self")'>1</text>
<line
x1='39.960' y1='39.960' x2='89.880' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='26.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k0", "_self")'>0</text>
</svg></div>
<pre>(defprotocol woolam basic
(defrole init
(vars (a s name) (n text))
(trace (send a) (recv n) (send (enc n (ltk a s))))
(non-orig (ltk a s)))
(defrole resp
(vars (a s b name) (n text))
(trace (recv a) (send n) (recv (enc n (ltk a s)))
(send (enc a (enc n (ltk a s)) (ltk b s)))
(recv (enc a n (ltk b s))))
(non-orig (ltk b s))
(uniq-orig n))
(defrole serv
(vars (a s b name) (n text))
(trace (recv (enc a (enc n (ltk a s)) (ltk b s)))
(send (enc a n (ltk b s))))))</pre>
<p id="k0">Item <a href="#t0">0</a>, Child: <a href="#k1">1</a>.</p>
<div>
<svg
class='diagram' width='79.920pt' height='454.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='414.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc a n (ltk b s))</title>
<circle style='fill: red;' cx='39.960' cy='414.960' r='6.000'/></g>
<g><title>(enc a (enc n (ltk a s)) (ltk b s))</title>
<circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>(enc n (ltk a s))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>a</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n n) (a a) (s s) (b b))</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;'>woolam 0</text>
</svg></div>
<pre>(defskeleton woolam
(vars (n text) (a s b name))
(defstrand resp 5 (n n) (a a) (s s) (b b))
(non-orig (ltk a s) (ltk b s))
(uniq-orig n)
(label 0)
(unrealized (0 2) (0 4))
(origs (n (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k1">Item <a href="#t0">1</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k2">2</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='454.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 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='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='414.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 n (ltk a s))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>n</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>a</title><circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc a n (ltk b s))</title>
<circle style='fill: red;' cx='39.960' cy='414.960' r='6.000'/></g>
<g><title>(enc a (enc n (ltk a s)) (ltk b s))</title>
<circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>(enc n (ltk a s))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>n</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>a</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n n) (a a) (s s))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n n) (a a) (s s) (b b))</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;'>woolam 1</text>
</svg></div>
<pre>(defskeleton woolam
(vars (n text) (a s b name))
(defstrand resp 5 (n n) (a a) (s s) (b b))
(defstrand init 3 (n n) (a a) (s s))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (ltk a s) (ltk b s))
(uniq-orig n)
(operation encryption-test (added-strand init 3) (enc n (ltk a s))
(0 2))
(label 1)
(parent 0)
(unrealized (0 4))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k2">Item <a href="#t0">2</a>, Parent: <a href="#k1">1</a>, Child: <a href="#k3">3</a>.</p>
<div>
<svg
class='diagram' width='279.840pt' height='454.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.840 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='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='264.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 239.880 264.960 Q 142.320 300.660 44.759 411.359'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc a n (ltk b s))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(enc a (enc n (ltk a s)) (ltk b s))</title>
<circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<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 n (ltk a s))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>n</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>a</title><circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc a n (ltk b s))</title>
<circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
<g><title>(enc a (enc n (ltk a s)) (ltk b s))</title>
<circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>(enc n (ltk a s))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-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>n</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>a</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n n) (a a) (s s) (b b))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
</g>
<g><title>((n n) (a a) (s s))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n n) (a a) (s s) (b b))</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;'>woolam 2</text>
</svg></div>
<pre>(defskeleton woolam
(vars (n text) (a s b name))
(defstrand resp 5 (n n) (a a) (s s) (b b))
(defstrand init 3 (n n) (a a) (s s))
(defstrand serv 2 (n n) (a a) (s s) (b b))
(precedes ((0 1) (1 1)) ((0 1) (2 0)) ((1 2) (0 2)) ((2 1) (0 4)))
(non-orig (ltk a s) (ltk b s))
(uniq-orig n)
(operation encryption-test (added-strand serv 2) (enc a n (ltk b s))
(0 4))
(label 2)
(parent 1)
(unrealized (2 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k3">Item <a href="#t0">3</a>, Parent: <a href="#k2">2</a>.</p>
<div>
<svg
class='diagram' width='279.840pt' height='454.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.840 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='239.880' y1='339.960' x2='239.880' y2='414.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='414.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 414.960 Q 142.920 377.460 45.960 414.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc a n (ltk b s))</title>
<circle cx='239.880' cy='414.960' r='6.000'/></g>
<g><title>(enc a (enc n (ltk a s)) (ltk b s))</title>
<circle style='fill: blue;' cx='239.880' cy='339.960' r='6.000'/></g>
<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 n (ltk a s))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>n</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>a</title><circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc a n (ltk b s))</title>
<circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
<path
d='M 39.960 339.960 Q 136.920 302.460 233.880 339.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc a (enc n (ltk a s)) (ltk b s))</title>
<circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>(enc n (ltk a s))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>n</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>a</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n n) (a a) (s s) (b b))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
</g>
<g><title>((n n) (a a) (s s))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n n) (a a) (s s) (b b))</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;'>woolam 3 (realized)</text></svg></div>
<pre>(defskeleton woolam
(vars (n text) (a s b name))
(defstrand resp 5 (n n) (a a) (s s) (b b))
(defstrand init 3 (n n) (a a) (s s))
(defstrand serv 2 (n n) (a a) (s s) (b b))
(precedes ((0 1) (1 1)) ((0 3) (2 0)) ((1 2) (0 2)) ((2 1) (0 4)))
(non-orig (ltk a s) (ltk b s))
(uniq-orig n)
(operation encryption-test (displaced 3 0 resp 4)
(enc a (enc n (ltk a s)) (ltk b s)) (2 0))
(label 3)
(parent 2)
(unrealized)
(shape)
(maps ((0) ((a a) (s s) (b b) (n n))))
(origs (n (0 1))))</pre>
</body>
</html>