cpsa-3.4.0: doc/examples/goals.xhtml
<?xml version="1.0"?>
<!-- CPSA 3.4.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>goals</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 goals)
(comment "CPSA 3.4.0")
(comment "All input read from goals.scm")</pre>
<p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t4">4</a> <a href="#t6">6</a> <a href="#t8">8</a> <a href="#t17">17</a> <a href="#t19">19</a> <a href="#t21">21</a> <a href="#t23">23</a> <a href="#t26">26</a> <a href="#t28">28</a> <a href="#t33">33</a> <a href="#t41">41</a> <a href="#t45">45</a> <a href="#t47">47</a> <a href="#t49">49</a> <a href="#t52">52</a> <a href="#t54">54</a> <a href="#t57">57</a> <a href="#t62">62</a> <a href="#t65">65</a>.</p>
<p id="t0">Tree <a href="#top">0</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
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 ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</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='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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 0</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (b a name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk b))
(uniq-orig n1)
(goals
(forall ((b name) (n1 text) (z0 node))
(implies
(and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)
(non (privk b)) (uniq n1))
(exists ((z1 node))
(and (p "resp" 1 z1) (p "resp" "b" z1 b))))))
(comment "Initiator point of view"
"Authentication goal: agreement on name b")
(label 0)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k1">Item <a href="#t0">1</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 1 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (b a name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 1)
(parent 0)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
(origs (n1 (0 0))))</pre>
<p id="t2">Tree <a href="#top">2</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k3", "_self")'>3</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("#k2", "_self")'>2</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k2">Item <a href="#t2">2</a>, Child: <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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 2</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (b a name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk b))
(uniq-orig n1)
(goals
(forall ((b name) (n1 text) (z0 node))
(implies
(and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)
(non (privk b)) (uniq n1))
(exists ((z1 node))
(and (p "resp" 1 z1) (p "resp" "b" z1 b) (prec z1 z0))))))
(comment "Prec example")
(label 2)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k3">Item <a href="#t2">3</a>, Parent: <a href="#k2">2</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>(enc n1 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 3 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (b a name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 3)
(parent 2)
(unrealized)
(shape)
(satisfies (no (b b) (n1 n1) (z0 (0 2))))
(maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))
(origs (n1 (0 0))))</pre>
<p id="t4">Tree <a href="#top">4</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k5", "_self")'>5</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("#k4", "_self")'>4</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k4">Item <a href="#t4">4</a>, Child: <a href="#k5">5</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 n2 (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns 4</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk a))
(uniq-orig n2)
(goals
(forall ((a b name) (n2 text) (z0 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
(p "resp" "b" z0 b) (non (privk a)) (uniq n2))
(exists ((z1 node))
(and (p "init" 1 z1) (p "init" "b" z1 b))))))
(comment "Responder point of view"
"Failed authentication goal: agreement on name b")
(label 4)
(unrealized (0 2))
(origs (n2 (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k5">Item <a href="#t4">5</a>, Parent: <a href="#k4">4</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 (pubk b-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns 5 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b b-0 name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (privk a))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (0 2)
(enc n1 n2 (pubk a)))
(label 5)
(parent 4)
(unrealized)
(shape)
(satisfies (no (a a) (b b) (n2 n2) (z0 (0 2))))
(maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
(origs (n2 (0 1))))</pre>
<p id="t6">Tree <a href="#top">6</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k7", "_self")'>7</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("#k6", "_self")'>6</text>
</svg></div>
<pre>(defprotocol nsl basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
(recv (enc n2 (pubk b)))))
(comment
"Needham-Schroeder-Lowe with no role origination assumptions"))</pre>
<p id="k6">Item <a href="#t6">6</a>, Child: <a href="#k7">7</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 n2 (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 b (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>nsl 6</text>
</svg></div>
<pre>(defskeleton nsl
(vars (n2 n1 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk a))
(uniq-orig n2)
(goals
(forall ((a b name) (n2 text) (z0 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
(p "resp" "b" z0 b) (non (privk a)) (uniq n2))
(exists ((z1 node))
(and (p "init" 1 z1) (p "init" "b" z1 b))))))
(comment "Responder point of view"
"Authentication goal: agreement on name b")
(label 6)
(unrealized (0 2))
(origs (n2 (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k7">Item <a href="#t6">7</a>, Parent: <a href="#k6">6</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 n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 b (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 b (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>nsl 7 (realized)</text></svg></div>
<pre>(defskeleton nsl
(vars (n2 n1 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (privk a))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (0 2)
(enc n1 n2 b (pubk a)))
(label 7)
(parent 6)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
(origs (n2 (0 1))))</pre>
<p id="t8">Tree <a href="#top">8</a>.</p>
<div>
<svg
class='diagram' width='379.440pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.440 229.920' font-size='12.000'>
<text
x='289.560' y='176.040'
style='font-style: italic; text-anchor: middle; fill: orange;'
onclick='window.open("#k15", "_self")'>15</text>
<line
x1='239.640' y1='189.960' x2='289.560' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='239.640' y='176.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k13", "_self")'>13</text>
<line
x1='189.720' y1='114.960' x2='239.640' y2='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='339.480' y='101.040'
style='font-style: italic; text-anchor: middle; fill: orange;'
onclick='window.open("#k16", "_self")'>16</text>
<line
x1='289.560' y1='114.960' x2='339.480' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='289.560' y='101.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k15", "_self")'>15</text>
<line
x1='239.640' y1='77.460' x2='289.560' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='339.480' y='26.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k16", "_self")'>16</text>
<line
x1='289.560' y1='39.960' x2='339.480' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='289.560' y='26.040' style='text-anchor: middle; fill: red;'
onclick='window.open("#k14", "_self")'>14</text>
<line
x1='239.640' y1='77.460' x2='289.560' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='239.640' y='63.540' style='text-anchor: middle; fill: red;'
onclick='window.open("#k12", "_self")'>12</text>
<line
x1='189.720' y1='114.960' x2='239.640' y2='77.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k11", "_self")'>11</text>
<line
x1='139.800' y1='114.960' x2='189.720' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k10", "_self")'>10</text>
<line
x1='89.880' y1='114.960' x2='139.800' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k9", "_self")'>9</text>
<line
x1='39.960' y1='114.960' x2='89.880' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k8", "_self")'>8</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k8">Item <a href="#t8">8</a>, Child: <a href="#k9">9</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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='89.940' y='39.960' style='text-anchor: middle;'>ns 8</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(goals
(forall ((a b name) (n1 text) (z0 z1 node))
(implies
(and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "a" z0 a)
(p "init" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n1)
(non (privk a)) (non (privk b)) (uniq n1)) (false))))
(comment "Initiator point of view"
"Secrecy goal: nonce n1 not revealed")
(label 8)
(unrealized (0 0) (1 1))
(preskeleton)
(comment "Not a skeleton"))</pre>
<p id="k9">Item <a href="#t8">9</a>, Parent: <a href="#k8">8</a>, Child: <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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='89.940' y='39.960' style='text-anchor: middle;'>ns 9</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(precedes ((1 0) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(goals
(forall ((a b name) (n1 text) (z0 z1 node))
(implies
(and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "a" z0 a)
(p "init" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n1)
(non (privk a)) (non (privk b)) (uniq n1)) (false))))
(comment "Initiator point of view"
"Secrecy goal: nonce n1 not revealed")
(label 9)
(parent 8)
(unrealized (0 0) (1 1))
(origs (n1 (1 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k10">Item <a href="#t8">10</a>, Parent: <a href="#k9">9</a>, Child: <a href="#k11">11</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='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='189.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>(enc n1 n2-0 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 139.920 114.960 Q 186.900 114.960 233.880 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='139.920' y='39.960' style='text-anchor: middle;'>ns 10</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (1 1)
(enc n1 a (pubk b)))
(label 10)
(parent 9)
(unrealized (0 0) (1 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k11">Item <a href="#t8">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='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='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='189.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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 139.920 114.960 Q 186.900 114.960 233.880 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='139.920' y='39.960' style='text-anchor: middle;'>ns 11</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (contracted (n2-0 n2)) n1 (1 1)
(enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
(label 11)
(parent 10)
(unrealized (0 0))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k12">Item <a href="#t8">12</a>, Parent: <a href="#k11">11</a>, Children: <a href="#k14">14</a> <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='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='189.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 189.960 Q 142.920 152.460 45.960 189.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 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='139.920' y='39.960' style='text-anchor: middle;'>ns 12</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((1 0) (2 0)) ((2 1) (0 0)) ((2 1) (1 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (displaced 3 2 resp 2) n1 (0 0)
(enc n1 a (pubk b)))
(label 12)
(parent 11)
(unrealized (0 0))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k13">Item <a href="#t8">13</a>, Parent: <a href="#k11">11</a>, Seen Child: <a href="#k15">15</a>.</p>
<div>
<svg
class='diagram' width='379.800pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.800 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='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='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='189.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 339.840 189.960 Q 192.900 152.460 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>(enc n1 n2-0 (pubk a))</title>
<circle cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
<path
d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='189.900' y='39.960' style='text-anchor: middle;'>ns 13</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((1 0) (2 0)) ((1 0) (3 0)) ((2 1) (1 1)) ((3 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 0)
(enc n1 a (pubk b)))
(label 13)
(parent 11)
(seen 15)
(unrealized (0 0))
(comment "1 in cohort - 0 not yet seen"))</pre>
<p id="k14">Item <a href="#t8">14</a>, Parent: <a href="#k12">12</a>, Child: <a href="#k16">16</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='264.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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n2 a (pubk b))</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>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n2 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n2) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n2) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='139.920' y='39.960' style='text-anchor: middle;'>ns 14</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 text) (a b name))
(deflistener n2)
(defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))
(precedes ((1 0) (2 0)) ((1 2) (0 0)) ((2 1) (1 1)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (displaced 3 1 init 3) n2 (0 0)
(enc n2 n2 (pubk a)) (enc n2 a (pubk b)))
(label 14)
(parent 12)
(unrealized (0 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k15">Item <a href="#t8">15</a>, Parent: <a href="#k12">12</a>, Seen Child: <a href="#k16">16</a>.</p>
<div>
<svg
class='diagram' width='379.800pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.800 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='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='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='189.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 339.840 189.960 Q 192.900 152.460 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>(enc n1 n2-0 (pubk a))</title>
<circle cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
<path
d='M 239.880 189.960 Q 142.920 152.460 45.960 189.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 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n1</title><circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n1</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='189.900' y='39.960' style='text-anchor: middle;'>ns 15</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (a b name))
(deflistener n1)
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((1 0) (2 0)) ((1 0) (3 0)) ((2 1) (0 0)) ((2 1) (1 1))
((3 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 0)
(enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
(label 15)
(parent 12)
(seen 16)
(unrealized (0 0))
(comment "1 in cohort - 0 not yet seen"))</pre>
<p id="k16">Item <a href="#t8">16</a>, Parent: <a href="#k14">14</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='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='264.960' x2='39.960' y2='339.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 339.840 189.960 Q 192.810 189.232 45.781 263.504'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 n2-0 (pubk a))</title>
<circle cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(enc n2 a (pubk b))</title>
<circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
<path
d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n2 a (pubk b))</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>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n2 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 139.920 114.960 Q 236.880 77.460 333.840 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n2) (b b) (a a))</title>
<text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n2 n2) (n1 n2) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n2) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<text x='189.900' y='39.960' style='text-anchor: middle;'>ns 16</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n2-0 text) (a b name))
(deflistener n2)
(defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))
(defstrand resp 2 (n2 n2-0) (n1 n2) (b b) (a a))
(precedes ((1 0) (2 0)) ((1 0) (3 0)) ((1 2) (0 0)) ((2 1) (1 1))
((3 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (added-strand resp 2) n2 (0 0) (enc n2 (pubk b))
(enc n2 n2 (pubk a)) (enc n2 a (pubk b)))
(label 16)
(parent 14)
(unrealized (0 0))
(comment "empty cohort"))</pre>
<p id="t17">Tree <a href="#top">17</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k18", "_self")'>18</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("#k17", "_self")'>17</text>
</svg></div>
<pre>(defprotocol unilateral basic
(defrole init
(vars (a name) (n text))
(trace (send (enc n (pubk a))) (recv n)))
(defrole resp
(vars (a name) (n text))
(trace (recv (enc n (pubk a))) (send n)))
(comment "Unilateral authentication"))</pre>
<p id="k17">Item <a href="#t17">17</a>, Child: <a href="#k18">18</a>.</p>
<div>
<svg
class='diagram' width='79.920pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 79.920 229.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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>n</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n (pubk a))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n n) (a a))</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;'>unilateral 17</text></svg></div>
<pre>(defskeleton unilateral
(vars (n text) (a name))
(defstrand init 2 (n n) (a a))
(non-orig (privk a))
(uniq-orig n)
(goals
(forall ((a name) (n text) (z0 node))
(implies
(and (p "init" 1 z0) (p "init" "n" z0 n) (p "init" "a" z0 a)
(non (privk a)) (uniq n))
(exists ((z1 node))
(and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
(comment "Unilateral authentication goal")
(label 17)
(unrealized (0 1))
(origs (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k18">Item <a href="#t17">18</a>, Parent: <a href="#k17">17</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 229.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='189.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>n</title><circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n</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>(enc n (pubk a))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n n) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n n) (a a))</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;'>unilateral 18 (realized)</text></svg>
</div>
<pre>(defskeleton unilateral
(vars (n text) (a name))
(defstrand init 2 (n n) (a a))
(defstrand resp 2 (n n) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a))
(uniq-orig n)
(operation nonce-test (added-strand resp 2) n (0 1) (enc n (pubk a)))
(label 18)
(parent 17)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((a a) (n n))))
(origs (n (0 0))))</pre>
<p id="t19">Tree <a href="#top">19</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k20", "_self")'>20</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("#k19", "_self")'>19</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k19">Item <a href="#t19">19</a>, Child: <a href="#k20">20</a>.</p>
<div>
<svg
class='diagram' width='79.920pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 79.920 229.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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n n2 (pubk a-0))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n a-0 (pubk a))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n) (n2 n2) (a a-0) (b a))</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;'>ns 19</text>
</svg></div>
<pre>(defskeleton ns
(vars (n n2 text) (a a-0 name))
(defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
(non-orig (privk a))
(uniq-orig n)
(goals
(forall ((a name) (n text) (z0 node))
(implies
(and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "b" z0 a)
(non (privk a)) (uniq n))
(exists ((z1 node))
(and (p "resp" 1 z1) (p "resp" "b" z1 a))))))
(comment "Initiator authentication goal"
"Same as unilateral goal under the predicate mapping:"
(p "init" "n") "->" (p "init" "n1") "and" (p "init" "a") "->"
(p "init" "b") "and" (p "resp" "a") "->" (p "resp" "b"))
(label 19)
(unrealized (0 1))
(origs (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k20">Item <a href="#t19">20</a>, Parent: <a href="#k19">19</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 229.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='189.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>(enc n n2-0 (pubk a-0))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n a-0 (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n n2 (pubk a-0))</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>(enc n a-0 (pubk a))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n) (b a) (a a-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n) (n2 n2) (a a-0) (b a))</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;'>ns 20 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n n2 n2-0 text) (a a-0 name))
(defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))
(defstrand resp 2 (n2 n2-0) (n1 n) (b a) (a a-0))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a))
(uniq-orig n)
(operation nonce-test (added-strand resp 2) n (0 1)
(enc n a-0 (pubk a)))
(label 20)
(parent 19)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((a a) (n n) (a-0 a-0) (n2 n2))))
(origs (n (0 0))))</pre>
<p id="t21">Tree <a href="#top">21</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k22", "_self")'>22</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("#k21", "_self")'>21</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k21">Item <a href="#t21">21</a>, Child: <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 n (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n) (n1 n1) (b b) (a a))</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;'>ns 21</text>
</svg></div>
<pre>(defskeleton ns
(vars (n n1 text) (a b name))
(defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
(non-orig (privk a))
(uniq-orig n)
(goals
(forall ((a name) (n text) (z0 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
(non (privk a)) (uniq n))
(exists ((z1 node))
(and (p "init" 2 z1) (p "init" "a" z1 a))))))
(comment "Responder authentication goal"
"Same as unilateral goal under the predicate mapping:" (p "init" 1)
"->" (p "resp" 2) "and" (p "init" "n") "->" (p "resp" "n2") "and"
(p "init" "a") "->" (p "resp" "a") "and" (p "resp" 1) "->"
(p "init" 2) "and" (p "resp" "a") "->" (p "init" "a"))
(label 21)
(unrealized (0 2))
(origs (n (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k22">Item <a href="#t21">22</a>, Parent: <a href="#k21">21</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n (pubk b-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n) (n1 n1) (b b) (a a))</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;'>ns 22 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n n1 text) (a b b-0 name))
(defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (privk a))
(uniq-orig n)
(operation nonce-test (added-strand init 3) n (0 2)
(enc n1 n (pubk a)))
(label 22)
(parent 21)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((a a) (n n) (b b) (n1 n1))))
(origs (n (0 1))))</pre>
<p id="t23">Tree <a href="#top">23</a>.</p>
<div>
<svg
class='diagram' width='179.760pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.760 79.920' font-size='12.000'>
<text
x='139.800' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k25", "_self")'>25</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("#k24", "_self")'>24</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("#k23", "_self")'>23</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k23">Item <a href="#t23">23</a>, Child: <a href="#k24">24</a>.</p>
<div>
<svg
class='diagram' width='79.920pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 79.920 229.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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n) (n2 n2) (a a) (b b))</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;'>ns 23</text>
</svg></div>
<pre>(defskeleton ns
(vars (n n2 text) (a b name))
(defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
(non-orig (privk a) (privk b))
(uniq-orig n)
(goals
(forall ((a b name) (n text) (z0 node))
(implies
(and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
(p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
(exists ((z1 node)) (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))
(forall ((a b name) (n text) (z0 node))
(implies
(and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)
(p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
(exists ((z1 node))
(and (p "resp" 1 z1) (p "resp" "a" z1 a))))))
(comment "Two initiator authentication goals")
(label 23)
(unrealized (0 1))
(origs (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k24">Item <a href="#t23">24</a>, Parent: <a href="#k23">23</a>, Child: <a href="#k25">25</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 229.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='189.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>(enc n n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n) (n2 n2) (a a) (b b))</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;'>ns 24</text>
</svg></div>
<pre>(defskeleton ns
(vars (n n2 n2-0 text) (a b name))
(defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n)
(operation nonce-test (added-strand resp 2) n (0 1)
(enc n a (pubk b)))
(label 24)
(parent 23)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k25">Item <a href="#t23">25</a>, Parent: <a href="#k24">24</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 229.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='189.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>(enc n n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n n2 (pubk a))</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>(enc n a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n) (n2 n2) (a a) (b b))</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;'>ns 25 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n n2 text) (a b name))
(defstrand init 2 (n1 n) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n)
(operation nonce-test (contracted (n2-0 n2)) n (0 1)
(enc n n2 (pubk a)) (enc n a (pubk b)))
(label 25)
(parent 24)
(unrealized)
(shape)
(satisfies yes yes)
(maps ((0) ((a a) (b b) (n n) (n2 n2))))
(origs (n (0 0))))</pre>
<p id="t26">Tree <a href="#top">26</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k27", "_self")'>27</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("#k26", "_self")'>26</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k26">Item <a href="#t26">26</a>, Child: <a href="#k27">27</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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 26</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (b a name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk b))
(uniq-orig n1)
(goals
(forall ((n1 n2 text) (b a name) (z z-0 node))
(implies
(and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
(p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
(p "init" "b" z-0 b) (str-prec z z-0) (non (privk b))
(uniq-at n1 z))
(exists ((n2-0 text) (z-1 z-2 z-3 node))
(and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)
(p "resp" "n2" z-3 n2-0) (p "resp" "n1" z-3 n1)
(p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)
(prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)
(str-prec z-2 z-3))))))
(comment "Shape analysis sentence")
(label 26)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k27">Item <a href="#t26">27</a>, Parent: <a href="#k26">26</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>(enc n1 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 27 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (b a name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 27)
(parent 26)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((n1 n1) (n2 n2) (b b) (a a))))
(origs (n1 (0 0))))</pre>
<p id="t28">Tree <a href="#top">28</a>.</p>
<div>
<svg
class='diagram' width='229.680pt' height='154.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 229.680 154.920' font-size='12.000'>
<text
x='189.720' y='101.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k32", "_self")'>32</text>
<line
x1='139.800' y1='77.460' x2='189.720' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k31", "_self")'>31</text>
<line
x1='139.800' y1='77.460' x2='189.720' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='63.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k30", "_self")'>30</text>
<line
x1='89.880' y1='77.460' x2='139.800' y2='77.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='63.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k29", "_self")'>29</text>
<line
x1='39.960' y1='77.460' x2='89.880' y2='77.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='63.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k28", "_self")'>28</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k28">Item <a href="#t28">28</a>, Child: <a href="#k29">29</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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: red;' cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text x='89.940' y='39.960' style='text-anchor: middle;'>ns 28</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b name))
(deflistener n2)
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(goals
(forall ((a b name) (n2 text) (z0 z1 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
(p "resp" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n2)
(non (privk a)) (non (privk b)) (uniq n2)) (false))))
(comment "Responder point of view"
"Failed secrecy goal: nonce n2 not revealed")
(label 28)
(unrealized (0 0) (1 2))
(preskeleton)
(comment "Not a skeleton"))</pre>
<p id="k29">Item <a href="#t28">29</a>, Parent: <a href="#k28">28</a>, Child: <a href="#k30">30</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='189.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: red;' cx='139.920' cy='264.960' r='6.000'/></g>
<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>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text x='89.940' y='39.960' style='text-anchor: middle;'>ns 29</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b name))
(deflistener n2)
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((1 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(goals
(forall ((a b name) (n2 text) (z0 z1 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)
(p "resp" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n2)
(non (privk a)) (non (privk b)) (uniq n2)) (false))))
(comment "Responder point of view"
"Failed secrecy goal: nonce n2 not revealed")
(label 29)
(parent 28)
(unrealized (0 0) (1 2))
(origs (n2 (1 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k30">Item <a href="#t28">30</a>, Parent: <a href="#k29">29</a>, Children: <a href="#k31">31</a> <a href="#k32">32</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='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='264.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>(enc n2 (pubk b-0))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<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;'/>
<path
d='M 139.920 189.960 Q 186.900 189.960 233.880 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text x='139.920' y='39.960' style='text-anchor: middle;'>ns 30</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b b-0 name))
(deflistener n2)
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(precedes ((1 1) (0 0)) ((1 1) (2 1)) ((2 2) (1 2)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (1 2)
(enc n1 n2 (pubk a)))
(label 30)
(parent 29)
(unrealized (0 0))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k31">Item <a href="#t28">31</a>, Parent: <a href="#k30">30</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='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='264.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;'/>
<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>(enc n2 (pubk b-0))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 189.960 Q 186.900 189.960 233.880 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>ns 31 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b b-0 name))
(deflistener n2)
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(precedes ((1 1) (2 1)) ((2 2) (0 0)) ((2 2) (1 2)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (displaced 3 2 init 3) n2 (0 0)
(enc n1 n2 (pubk a)))
(label 31)
(parent 30)
(unrealized)
(shape)
(satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))
(maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))
(origs (n2 (1 1))))</pre>
<p id="k32">Item <a href="#t28">32</a>, Parent: <a href="#k30">30</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='264.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='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='264.960' x2='39.960' y2='339.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 339.840 264.960 Q 192.900 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 n2 (pubk b-1))</title>
<circle cx='339.840' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-1))</title>
<circle 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>(enc n2 (pubk b-0))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 189.960 Q 186.900 189.960 233.880 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<path
d='M 139.920 189.960 Q 236.880 152.460 333.840 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-1))</title>
<text x='339.840' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text
x='189.900' y='39.960'
style='text-anchor: middle;'>ns 32 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b b-0 b-1 name))
(deflistener n2)
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-1))
(precedes ((1 1) (2 1)) ((1 1) (3 1)) ((2 2) (1 2)) ((3 2) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (0 0)
(enc n1 n2 (pubk a)))
(label 32)
(parent 30)
(unrealized)
(shape)
(satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))
(maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))
(origs (n2 (1 1))))</pre>
<p id="t33">Tree <a href="#top">33</a>.</p>
<div>
<svg
class='diagram' width='279.600pt' height='154.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.600 154.920' font-size='12.000'>
<text
x='239.640' y='101.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k40", "_self")'>40</text>
<line
x1='189.720' y1='114.960' x2='239.640' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k39", "_self")'>39</text>
<line
x1='139.800' y1='114.960' x2='189.720' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k37", "_self")'>37</text>
<line
x1='89.880' y1='114.960' x2='139.800' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='89.880' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k35", "_self")'>35</text>
<line
x1='39.960' y1='77.460' x2='89.880' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k38", "_self")'>38</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("#k36", "_self")'>36</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("#k34", "_self")'>34</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("#k33", "_self")'>33</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k33">Item <a href="#t33">33</a>, Children: <a href="#k34">34</a> <a href="#k35">35</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;'/>
<g><title>(enc n2-0 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1-0 n2-0 (pubk a))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1-0 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1-0) (n2 n2-0) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 33</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n1-0 n2 n2-0 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
(non-orig (privk a) (privk b))
(uniq-orig n1 n1-0)
(subgoals
(forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))
(implies
(and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)
(p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)
(p "init" "a" z-0 a) (p "init" "b" z-0 b)
(p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)
(p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)
(str-prec z-1 z-2) (non (privk a)) (non (privk b))
(uniq-at n1 z) (uniq-at n1-0 z-1)) (= z-1 z))))
(comment "Double initiator point of view")
(label 33)
(unrealized (0 1) (1 1))
(origs (n1 (0 0)) (n1-0 (1 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k34">Item <a href="#t33">34</a>, Parent: <a href="#k33">33</a>, Child: <a href="#k36">36</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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 34</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation collapsed 1 0)
(label 34)
(parent 33)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k35">Item <a href="#t33">35</a>, Parent: <a href="#k33">33</a>, Child: <a href="#k37">37</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='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='264.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>(enc n1-0 n2-1 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1-0 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2-0 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1-0 n2-0 (pubk a))</title>
<circle style='fill: red;' 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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-1) (n1 n1-0) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1-0) (n2 n2-0) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 35</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
(defstrand resp 2 (n2 n2-1) (n1 n1-0) (b b) (a a))
(precedes ((1 0) (2 0)) ((2 1) (1 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1 n1-0)
(operation nonce-test (added-strand resp 2) n1-0 (1 1)
(enc n1-0 a (pubk b)))
(label 35)
(parent 33)
(unrealized (0 1) (1 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k36">Item <a href="#t33">36</a>, Parent: <a href="#k34">34</a>, Child: <a href="#k38">38</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>(enc n1 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 36</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 36)
(parent 34)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k37">Item <a href="#t33">37</a>, Parent: <a href="#k35">35</a>, Child: <a href="#k39">39</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='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='264.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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 n2-0 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1-0 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2-0 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1-0 n2-0 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1-0) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1-0) (n2 n2-0) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 37</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n1-0 n2 n2-0 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a))
(precedes ((1 0) (2 0)) ((2 1) (1 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1 n1-0)
(operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1)
(enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b)))
(label 37)
(parent 35)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k38">Item <a href="#t33">38</a>, Parent: <a href="#k36">36</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>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 38 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
(enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
(label 38)
(parent 36)
(unrealized)
(shape)
(satisfies yes)
(maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))
(origs (n1 (0 0))))</pre>
<p id="k39">Item <a href="#t33">39</a>, Parent: <a href="#k37">37</a>, Child: <a href="#k40">40</a>.</p>
<div>
<svg
class='diagram' width='379.800pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.800 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='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='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='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 339.840 189.960 Q 192.900 152.460 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>(enc n1 n2-1 (pubk a))</title>
<circle cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
<path
d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 n2-0 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1-0 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2-0 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1-0 n2-0 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-1) (n1 n1) (b b) (a a))</title>
<text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n2 n2-0) (n1 n1-0) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1-0) (n2 n2-0) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 39</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a))
(defstrand resp 2 (n2 n2-1) (n1 n1) (b b) (a a))
(precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1 n1-0)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 39)
(parent 37)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k40">Item <a href="#t33">40</a>, Parent: <a href="#k39">39</a>.</p>
<div>
<svg
class='diagram' width='379.800pt' height='304.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 379.800 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='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='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='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 339.840 189.960 Q 192.900 152.460 45.960 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2-0 (pubk a))</title>
<circle cx='339.840' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
<path
d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 n2 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1-0 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1-0 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1-0 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2-0 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2-0 (pubk a))</title>
<circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 186.900 77.460 333.840 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n2 n2) (n1 n1-0) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1-0) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2-0) (a a) (b b))</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;'>ns 40 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n1-0 n2 n2-0 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))
(defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1 n1-0)
(operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)
(enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
(label 40)
(parent 39)
(unrealized)
(shape)
(satisfies
(no (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2) (a a) (b b) (z (0 0))
(z-0 (0 2)) (z-1 (1 0)) (z-2 (1 2))))
(maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))
(origs (n1 (0 0)) (n1-0 (1 0))))</pre>
<p id="t41">Tree <a href="#top">41</a>.</p>
<div>
<svg
class='diagram' width='179.760pt' height='154.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.760 154.920' font-size='12.000'>
<text
x='139.800' y='101.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k44", "_self")'>44</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='text-anchor: middle; fill: red;'
onclick='window.open("#k43", "_self")'>43</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("#k42", "_self")'>42</text>
<line
x1='39.960' y1='77.460' x2='89.880' y2='77.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='63.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k41", "_self")'>41</text>
</svg></div>
<pre>(defprotocol nsl-typeless basic
(defrole init
(vars (a b name) (n1 text) (n2 mesg))
(trace (send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 text) (n1 mesg))
(trace (recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder-Lowe with untyped nonces"))</pre>
<p id="k41">Item <a href="#t41">41</a>, Child: <a href="#k42">42</a>.</p>
<div>
<svg
class='diagram' width='179.880pt' height='229.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.880 229.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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<g><title>(enc n1 n2 b (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc a n1 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>nsl-typeless 41</text></svg></div>
<pre>(defskeleton nsl-typeless
(vars (n1 mesg) (n2 text) (a b name))
(deflistener n2)
(defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(goals
(forall ((n2 text) (a b name) (z z-0 node))
(implies
(and (p "resp" 1 z) (p "" 0 z-0) (p "resp" "n2" z n2)
(p "resp" "b" z b) (p "resp" "a" z a) (p "" "x" z-0 n2)
(non (privk a)) (non (privk b)) (uniq n2)) (false))))
(comment "Shows typeflaw in typeless NSL")
(label 41)
(unrealized (0 0))
(preskeleton)
(comment "Not a skeleton"))</pre>
<p id="k42">Item <a href="#t41">42</a>, Parent: <a href="#k41">41</a>, Children: <a href="#k43">43</a> <a href="#k44">44</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='189.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>(enc n1 n2 b (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc a n1 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>nsl-typeless 42</text></svg></div>
<pre>(defskeleton nsl-typeless
(vars (n1 mesg) (n2 text) (a b name))
(deflistener n2)
(defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
(precedes ((1 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(goals
(forall ((n2 text) (a b name) (z z-0 node))
(implies
(and (p "resp" 1 z) (p "" 0 z-0) (p "resp" "n2" z n2)
(p "resp" "b" z b) (p "resp" "a" z a) (p "" "x" z-0 n2)
(non (privk a)) (non (privk b)) (uniq n2)) (false))))
(comment "Shows typeflaw in typeless NSL")
(label 42)
(parent 41)
(unrealized (0 0))
(origs (n2 (1 1)))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k43">Item <a href="#t41">43</a>, Parent: <a href="#k42">42</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='264.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 n2 (pubk b))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 b (pubk a))</title>
<circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc a n1 (pubk b))</title>
<circle cx='239.880' cy='114.960' r='6.000'/></g>
<path
d='M 139.920 189.960 Q 186.900 189.960 233.880 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 b (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc a n1 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (a a) (b b))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n1 n1) (n2 n2) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>nsl-typeless 43</text></svg></div>
<pre>(defskeleton nsl-typeless
(vars (n2 n1 text) (a b name))
(deflistener n2)
(defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))
(defstrand init 3 (n2 n2) (n1 n1) (a a) (b b))
(precedes ((1 1) (2 1)) ((2 2) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (0 0)
(enc n1 n2 b (pubk a)))
(label 43)
(parent 42)
(unrealized (0 0))
(comment "empty cohort"))</pre>
<p id="k44">Item <a href="#t41">44</a>, Parent: <a href="#k42">42</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='189.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='264.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 (cat n2 b) n2-0 a (pubk a-0))</title>
<circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>(enc a-0 n2 b (pubk a))</title>
<circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
<path
d='M 139.920 189.960 Q 186.900 189.960 233.880 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc a-0 n2 b (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc a a-0 (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>n2</title><circle cx='39.960' cy='339.960' r='6.000'/></g>
<g><title>n2</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>((n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 a-0) (n2 n2) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>nsl-typeless 44 (realized)</text></svg>
</div>
<pre>(defskeleton nsl-typeless
(vars (n2 n2-0 text) (a b a-0 name))
(deflistener n2)
(defstrand resp 2 (n1 a-0) (n2 n2) (b b) (a a))
(defstrand resp 2 (n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))
(precedes ((1 1) (2 0)) ((2 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2)
(operation nonce-test (added-strand resp 2) n2 (0 0)
(enc a-0 n2 b (pubk a)))
(label 44)
(parent 42)
(unrealized)
(shape)
(satisfies (no (n2 n2) (a a) (b b) (z (1 1)) (z-0 (0 0))))
(maps ((0 1) ((n2 n2) (a a) (b b) (n1 a-0))))
(origs (n2 (1 1))))</pre>
<p id="t45">Tree <a href="#top">45</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k46", "_self")'>46</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("#k45", "_self")'>45</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k45">Item <a href="#t45">45</a>, Child: <a href="#k46">46</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 n2 (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns 45</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk a))
(uniq-orig n2)
(subgoals
(forall ((n1 n2 text) (a b name) (z z-0 node))
(implies
(and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
(p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
(p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
(non (privk b)) (uniq-at n1 z))
(exists ((z-1 z-2 z-3 node))
(and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)
(p "resp" "n2" z-3 n2) (p "resp" "n1" z-3 n1)
(p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)
(prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)
(str-prec z-2 z-3))))))
(comment "Responder point of view with SAS")
(label 45)
(unrealized (0 2))
(origs (n2 (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k46">Item <a href="#t45">46</a>, Parent: <a href="#k45">45</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 (pubk b-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns 46 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b b-0 name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (privk a))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (0 2)
(enc n1 n2 (pubk a)))
(label 46)
(parent 45)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
(origs (n2 (0 1))))</pre>
<p id="t47">Tree <a href="#top">47</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k48", "_self")'>48</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("#k47", "_self")'>47</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k47">Item <a href="#t47">47</a>, Child: <a href="#k48">48</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 n2 (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns 47</text>
</svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk a))
(uniq-orig n2)
(subgoals
(forall ((n1 n2 text) (a b name) (z z-0 node))
(implies
(and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
(p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
(p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
(non (privk b)) (uniq-at n1 z)) (false))))
(comment "Responder point of view with false as the conclusion")
(label 47)
(unrealized (0 2))
(origs (n2 (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k48">Item <a href="#t47">48</a>, Parent: <a href="#k47">47</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 (pubk b-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns 48 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n2 n1 text) (a b b-0 name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (privk a))
(uniq-orig n2)
(operation nonce-test (added-strand init 3) n2 (0 2)
(enc n1 n2 (pubk a)))
(label 48)
(parent 47)
(unrealized)
(shape)
(satisfies yes)
(maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
(origs (n2 (0 1))))</pre>
<p id="t49">Tree <a href="#top">49</a>.</p>
<div>
<svg
class='diagram' width='179.760pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.760 79.920' font-size='12.000'>
<text
x='139.800' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k51", "_self")'>51</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("#k50", "_self")'>50</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("#k49", "_self")'>49</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k49">Item <a href="#t49">49</a>, Child: <a href="#k50">50</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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 49</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(subgoals
(forall ((n1 n2 text) (a b name) (z z-0 node))
(implies
(and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)
(p "init" "n2" z-0 n2) (p "init" "a" z-0 a)
(p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))
(non (privk b)) (uniq-at n1 z)) (false))))
(comment "Initiator point of view with false as the conclusion")
(label 49)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k50">Item <a href="#t49">50</a>, Parent: <a href="#k49">49</a>, Child: <a href="#k51">51</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>(enc n1 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 50</text>
</svg></div>
<pre>(defskeleton ns
(vars (n1 n2 n2-0 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 50)
(parent 49)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k51">Item <a href="#t49">51</a>, Parent: <a href="#k50">50</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>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 51 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
(enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
(label 51)
(parent 50)
(unrealized)
(shape)
(satisfies (no (n1 n1) (n2 n2) (a a) (b b) (z (0 0)) (z-0 (0 2))))
(maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
(origs (n1 (0 0))))</pre>
<p id="t52">Tree <a href="#top">52</a>.</p>
<div>
<svg
class='diagram' width='129.840pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 129.840 79.920' font-size='12.000'>
<text
x='89.880' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k53", "_self")'>53</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("#k52", "_self")'>52</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k52">Item <a href="#t52">52</a>, Child: <a href="#k53">53</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 n (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n) (n1 n1) (b b) (a a))</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;'>ns 52</text>
</svg></div>
<pre>(defskeleton ns
(vars (n n1 text) (a b name))
(defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
(non-orig (privk a) (privk b))
(uniq-orig n)
(goals
(forall ((a b name) (n text) (z0 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
(p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
(exists ((z1 node)) (and (p "init" 2 z1) (p "init" "a" z1 a)))))
(forall ((a b name) (n text) (z0 node))
(implies
(and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)
(p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))
(exists ((z1 node))
(and (p "init" 2 z1) (p "init" "b" z1 b))))))
(comment "Two responder authentication goals")
(label 52)
(unrealized (0 2))
(origs (n (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k53">Item <a href="#t52">53</a>, Parent: <a href="#k52">52</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n (pubk b-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n) (n1 n1) (b b) (a a))</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;'>ns 53 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n n1 text) (a b b-0 name))
(defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))
(precedes ((0 1) (1 1)) ((1 2) (0 2)))
(non-orig (privk a) (privk b))
(uniq-orig n)
(operation nonce-test (added-strand init 3) n (0 2)
(enc n1 n (pubk a)))
(label 53)
(parent 52)
(unrealized)
(shape)
(satisfies yes (no (a a) (b b) (n n) (z0 (0 2))))
(maps ((0) ((a a) (b b) (n n) (n1 n1))))
(origs (n (0 1))))</pre>
<p id="t54">Tree <a href="#top">54</a>.</p>
<div>
<svg
class='diagram' width='179.760pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.760 79.920' font-size='12.000'>
<text
x='139.800' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k56", "_self")'>56</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("#k55", "_self")'>55</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("#k54", "_self")'>54</text>
</svg></div>
<pre>(defprotocol ns-role-origs basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b))))
(non-orig (privk b))
(uniq-orig n1))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b))))
(non-orig (privk a))
(uniq-orig n2))
(comment
"Needham-Schroeder with role assumptions that are too strong"))</pre>
<p id="k54">Item <a href="#t54">54</a>, Child: <a href="#k55">55</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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns-role-origs 54</text></svg></div>
<pre>(defskeleton ns-role-origs
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(non-orig (privk b))
(uniq-orig n1)
(label 54)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k55">Item <a href="#t54">55</a>, Parent: <a href="#k54">54</a>, Child: <a href="#k56">56</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>(enc n1 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns-role-origs 55</text></svg></div>
<pre>(defskeleton ns-role-origs
(vars (n1 n2 n2-0 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1 n2-0)
(operation nonce-test (added-strand resp 2) n1 (0 1)
(enc n1 a (pubk b)))
(label 55)
(parent 54)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k56">Item <a href="#t54">56</a>, Parent: <a href="#k55">55</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>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns-role-origs 56 (realized)</text></svg>
</div>
<pre>(defskeleton ns-role-origs
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1 n2)
(operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
(enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
(label 56)
(parent 55)
(unrealized)
(shape)
(maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
(origs (n2 (1 1)) (n1 (0 0))))</pre>
<p id="t57">Tree <a href="#top">57</a>.</p>
<div>
<svg
class='diagram' width='279.600pt' height='154.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 279.600 154.920' font-size='12.000'>
<text
x='239.640' y='101.040'
style='font-style: italic; text-anchor: middle; fill: green;'
onclick='window.open("#k59", "_self")'>59</text>
<line
x1='189.720' y1='114.960' x2='239.640' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='101.040' style='text-anchor: middle; fill: blue;'
onclick='window.open("#k61", "_self")'>61</text>
<line
x1='139.800' y1='114.960' x2='189.720' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='139.800' y='101.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k60", "_self")'>60</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("#k59", "_self")'>59</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("#k58", "_self")'>58</text>
<line
x1='39.960' y1='77.460' x2='89.880' y2='77.460'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='39.960' y='63.540' style='text-anchor: middle; fill: black;'
onclick='window.open("#k57", "_self")'>57</text>
</svg></div>
<pre>(defprotocol ns-role-origs basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b))))
(non-orig (privk b))
(uniq-orig n1))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b))))
(non-orig (privk a))
(uniq-orig n2))
(comment
"Needham-Schroeder with role assumptions that are too strong"))</pre>
<p id="k57">Item <a href="#t57">57</a>, Child: <a href="#k58">58</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 n2 (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns-role-origs 57</text></svg></div>
<pre>(defskeleton ns-role-origs
(vars (n2 n1 text) (b a name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(non-orig (privk a))
(uniq-orig n2)
(label 57)
(unrealized (0 2))
(origs (n2 (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k58">Item <a href="#t57">58</a>, Parent: <a href="#k57">57</a>, Children: <a href="#k59">59</a> <a href="#k60">60</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n2 (pubk b-0))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns-role-origs 58</text></svg></div>
<pre>(defskeleton ns-role-origs
(vars (n2 n1 text) (b a b-0 name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
(non-orig (privk a) (privk b-0))
(uniq-orig n2 n1)
(operation nonce-test (added-strand init 3) n2 (0 2)
(enc n1 n2 (pubk a)))
(label 58)
(parent 57)
(unrealized (0 0) (0 2))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k59">Item <a href="#t57">59</a>, Parent: <a href="#k58">58</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 n2 (pubk b))</title>
<circle cx='139.920' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns-role-origs 59 (realized)</text></svg>
</div>
<pre>(defskeleton ns-role-origs
(vars (n2 n1 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
(non-orig (privk a) (privk b))
(uniq-orig n2 n1)
(operation nonce-test (contracted (b-0 b)) n1 (0 0)
(enc n1 a (pubk b)))
(label 59)
(parent 58)
(unrealized)
(shape)
(maps ((0) ((b b) (a a) (n2 n2) (n1 n1))))
(origs (n1 (1 0)) (n2 (0 1))))</pre>
<p id="k60">Item <a href="#t57">60</a>, Parent: <a href="#k58">58</a>, Child: <a href="#k61">61</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='339.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 239.880 189.960 Q 142.920 152.460 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>(enc n1 n2-0 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b-0))</title>
<circle style='fill: blue;' cx='239.880' cy='114.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 n2 (pubk b-0))</title>
<circle cx='139.920' cy='339.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 186.900 114.960 233.880 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b-0))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
<path
d='M 39.960 264.960 Q 86.940 264.960 133.920 264.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b-0) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns-role-origs 60</text></svg></div>
<pre>(defskeleton ns-role-origs
(vars (n2 n1 n2-0 text) (b a b-0 name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b-0) (a a))
(precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
(non-orig (privk a) (privk b-0))
(uniq-orig n2 n1 n2-0)
(operation nonce-test (added-strand resp 2) n1 (0 0)
(enc n1 a (pubk b-0)))
(label 60)
(parent 58)
(unrealized (0 0) (0 2))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k61">Item <a href="#t57">61</a>, Parent: <a href="#k60">60</a>, Seen Child: <a href="#k59">59</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='339.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 239.880 189.960 Q 142.920 152.460 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>(enc n1 n2-0 (pubk a))</title>
<circle cx='239.880' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='239.880' cy='114.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 n2 (pubk b))</title>
<circle cx='139.920' cy='339.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 186.900 114.960 233.880 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 a (pubk b))</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
<path
d='M 39.960 264.960 Q 86.940 264.960 133.920 264.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n1 n2 (pubk a))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n1) (b b) (a a))</title>
<text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>init</text>
</g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</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;'>ns-role-origs 61 (realized)</text></svg>
</div>
<pre>(defskeleton ns-role-origs
(vars (n2 n1 n2-0 text) (a b name))
(defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
(precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
(non-orig (privk a) (privk b))
(uniq-orig n2 n1 n2-0)
(operation nonce-test (contracted (b-0 b)) n1 (0 0)
(enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))
(label 61)
(parent 60)
(seen 59)
(unrealized)
(comment "1 in cohort - 0 not yet seen"))</pre>
<p id="t62">Tree <a href="#top">62</a>.</p>
<div>
<svg
class='diagram' width='179.760pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 179.760 79.920' font-size='12.000'>
<text
x='139.800' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k64", "_self")'>64</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("#k63", "_self")'>63</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("#k62", "_self")'>62</text>
</svg></div>
<pre>(defprotocol ns2 basic
(defrole init
(vars (a b name) (n1 n2 n3 text))
(trace (send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b))))
(note doubled nonce in the first message))
(note that this protocol is derived from Needham-Schroeder))</pre>
<p id="k62">Item <a href="#t62">62</a>, Child: <a href="#k63">63</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 n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 n3 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n1 n1) (n2 n2) (n3 n3) (a a) (b b))</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;'>ns2 62</text>
</svg></div>
<pre>(defskeleton ns2
(vars (n1 n2 n3 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(label 62)
(unrealized (0 1))
(origs (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k63">Item <a href="#t62">63</a>, Parent: <a href="#k62">62</a>, Child: <a href="#k64">64</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>(enc n3 n2-0 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n3 n3 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n3 n2 (pubk a))</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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(enc n3 n3 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2-0) (n1 n3) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n3) (n2 n2) (n3 n3) (a a) (b b))</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;'>ns2 63</text>
</svg></div>
<pre>(defskeleton ns2
(vars (n2 n3 n2-0 text) (a b name))
(defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
(defstrand resp 2 (n2 n2-0) (n1 n3) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n3)
(operation nonce-test (added-strand resp 2) n3 (0 1)
(enc n3 n3 a (pubk b)))
(label 63)
(parent 62)
(unrealized (0 1))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k64">Item <a href="#t62">64</a>, Parent: <a href="#k63">63</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>(enc n3 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n3 n3 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n3 n2 (pubk a))</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>(enc n3 n3 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n3) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n3) (n2 n2) (n3 n3) (a a) (b b))</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;'>ns2 64 (realized)</text></svg></div>
<pre>(defskeleton ns2
(vars (n3 n2 text) (a b name))
(defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n3) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n3)
(operation nonce-test (contracted (n2-0 n2)) n3 (0 1)
(enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)))
(label 64)
(parent 63)
(unrealized)
(shape)
(maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))
(origs (n3 (0 0))))</pre>
<p id="t65">Tree <a href="#top">65</a>.</p>
<div>
<svg
class='diagram' width='79.920pt' height='79.920pt'
xmlns='http://www.w3.org/2000/svg' version='1.1'
viewBox='0 0 79.920 79.920' font-size='12.000'>
<text
x='39.960' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k65", "_self")'>65</text>
</svg></div>
<pre>(defprotocol ns basic
(defrole init
(vars (a b name) (n1 n2 text))
(trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
(send (enc n2 (pubk b)))))
(defrole resp
(vars (b a name) (n2 n1 text))
(trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
(recv (enc n2 (pubk b)))))
(comment "Needham-Schroeder with no role origination assumptions"))</pre>
<p id="k65">Item <a href="#t65">65</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>(enc n1 n2 (pubk a))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(enc n1 a (pubk b))</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g><title>(enc n2 (pubk b))</title>
<circle cx='39.960' cy='264.960' r='6.000'/></g>
<g><title>(enc n1 n2 (pubk a))</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>(enc n1 a (pubk b))</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g><title>((n2 n2) (n1 n1) (b b) (a a))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>resp</text>
</g>
<g><title>((n1 n1) (n2 n2) (a a) (b b))</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;'>ns 65 (realized)</text></svg></div>
<pre>(defskeleton ns
(vars (n1 n2 text) (a b name))
(defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
(defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk a) (privk b))
(uniq-orig n1)
(label 65)
(unrealized)
(shape)
(maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))
(origs (n1 (0 0))))</pre>
</body>
</html>