cpsa-3.6.2: doc/examples/pkinit.xhtml
<?xml version="1.0"?>
<!-- CPSA 3.6.2 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Kerberos PKINIT</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 "Kerberos PKINIT")
(comment "CPSA 3.6.2")
(comment "All input read from pkinit.scm")</pre>
<p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t8">8</a> <a href="#t13">13</a> <a href="#t16">16</a> <a href="#t23">23</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 pkinit-flawed basic
(defrole client
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (send (cat (enc tc n2 (privk c)) c t n1))
(recv
(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig n2 n1))
(defrole auth
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (recv (cat (enc tc n2 (privk c)) c t n1))
(send
(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig k ak)))</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='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>(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='39.960' y='39.960'
style='text-anchor: middle;'>pkinit-flawed 0</text></svg></div>
<pre>(defskeleton pkinit-flawed
(vars (n2 n1 text) (tc tk tgt data) (c as t name) (k ak skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1)
(goals
(forall ((c as name) (k skey) (z strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (non (privk as))
(non (privk c)))
(exists ((z-0 strd))
(and (p "auth" z-0 2) (p "auth" "as" z-0 as)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c))))))
(label 0)
(unrealized (0 1))
(origs (n1 (0 0)) (n2 (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='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>(cat (enc (enc k n2 (privk as)) (pubk c-0)) c-0 tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2 (privk c-0)) c-0 t-0 n1-0)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c-0) (t t-0) (as as) (k k) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-flawed 1 (realized)</text></svg>
</div>
<pre>(defskeleton pkinit-flawed
(vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c as t c-0 t-0 name) (k ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
(c c-0) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak-0)
(operation encryption-test (added-strand auth 2) (enc k n2 (privk as))
(0 1))
(label 1)
(parent 0)
(unrealized)
(shape)
(satisfies (no (c c) (as as) (k k) (z 0)))
(maps
((0)
((c c) (as as) (k k) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk)
(tgt tgt) (ak ak))))
(origs (k (1 1)) (ak-0 (1 1)) (n1 (0 0)) (n2 (0 0))))</pre>
<p id="t2">Tree <a href="#top">2</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='text-anchor: middle; fill: red;'
onclick='window.open("#k7", "_self")'>7</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: red;'
onclick='window.open("#k6", "_self")'>6</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("#k5", "_self")'>5</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("#k4", "_self")'>4</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("#k3", "_self")'>3</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("#k2", "_self")'>2</text>
</svg></div>
<pre>(defprotocol pkinit-fix1 basic
(defrole client
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (send (cat (enc tc n2 (privk c)) c t n1))
(recv
(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig n2 n1))
(defrole auth
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (recv (cat (enc tc n2 (privk c)) c t n1))
(send
(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig k ak)))</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='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>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='39.960' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 2</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 text) (tc tk tgt data) (c as t name) (k ak skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1)
(goals
(forall ((c as name) (k skey) (z strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (non (privk as))
(non (privk c)))
(exists ((z-0 strd))
(and (p "auth" z-0 2) (p "auth" "as" z-0 as)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c))))))
(label 2)
(unrealized (0 1))
(origs (n1 (0 0)) (n2 (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>, Child: <a href="#k4">4</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>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2 (privk c)) c t-0 n1-0)</title>
<circle style='fill: red;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 3</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c as t t-0 name) (k ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak-0)
(operation encryption-test (added-strand auth 2)
(enc k n2 c (privk as)) (0 1))
(label 3)
(parent 2)
(unrealized (0 1) (1 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k4">Item <a href="#t2">4</a>, Parent: <a href="#k3">3</a>, Children: <a href="#k5">5</a> <a href="#k6">6</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>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t-0 n1-0)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 4</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tk-0 tgt-0 data) (c as t t-0 name)
(k ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak-0)
(operation encryption-test (displaced 2 0 client 1)
(enc tc-0 n2 (privk c)) (1 0))
(label 4)
(parent 3)
(unrealized (0 1))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k5">Item <a href="#t2">5</a>, Parent: <a href="#k4">4</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>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</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>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 5 (realized)</text></svg>
</div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 text) (tc tgt tk tgt-0 data) (c as t name) (k ak skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
(t t) (as as) (k k) (ak ak))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (displaced 2 1 auth 2)
(enc ak-0 n1-0 tk-0 t-0 k) (0 1))
(label 5)
(parent 4)
(unrealized)
(shape)
(satisfies yes)
(maps
((0)
((c c) (as as) (k k) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk)
(tgt tgt) (ak ak))))
(origs (k (1 1)) (ak (1 1)) (n1 (0 0)) (n2 (0 0))))</pre>
<p id="k6">Item <a href="#t2">6</a>, Parent: <a href="#k4">4</a>, Child: <a href="#k7">7</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='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='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 45.960 264.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>k</title><circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>k</title>
<circle style='fill: red;' 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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t-0 n1-0)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 6</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tk-0 tgt-0 data) (c as t t-0 name)
(k ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k k) (ak ak-0))
(deflistener k)
(precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak-0)
(operation encryption-test (added-listener k) (enc ak n1 tk t k)
(0 1))
(label 6)
(parent 4)
(unrealized (2 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k7">Item <a href="#t2">7</a>, Parent: <a href="#k6">6</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='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='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 45.960 264.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>ak-0</title><circle cx='239.880' cy='264.960' r='6.000'/>
</g>
<g><title>ak-0</title>
<circle style='fill: red;' 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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc ak-0 n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 ak-0))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t-0 n1-0)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc ak-0 n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak-0))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k ak-0) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak-0) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 7</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tk-0 tgt-0 data) (c as t t-0 name)
(ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k ak-0) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k ak-0) (ak ak-0))
(deflistener ak-0)
(precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 ak-0)
(operation nonce-test (displaced 3 1 auth 2) k (2 0)
(enc (enc k n2 c (privk as)) (pubk c)))
(label 7)
(parent 6)
(unrealized (2 0))
(comment "empty cohort"))</pre>
<p id="t8">Tree <a href="#top">8</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='text-anchor: middle; fill: red;'
onclick='window.open("#k12", "_self")'>12</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: red;'
onclick='window.open("#k11", "_self")'>11</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("#k10", "_self")'>10</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("#k9", "_self")'>9</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("#k8", "_self")'>8</text>
</svg></div>
<pre>(defprotocol pkinit-fix2 basic
(defrole client
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (send (cat (enc tc n2 (privk c)) c t n1))
(recv
(cat
(enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
(pubk c)) c tgt (enc ak n1 tk t k))))
(uniq-orig n2 n1))
(defrole auth
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (recv (cat (enc tc n2 (privk c)) c t n1))
(send
(cat
(enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
(pubk c)) c tgt (enc ak n1 tk t k))))
(uniq-orig k ak)))</pre>
<p id="k8">Item <a href="#t8">8</a>, Child: <a href="#k9">9</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>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='39.960' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 8</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt data) (c as t name) (k ak skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1)
(goals
(forall ((c as name) (k skey) (z strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (non (privk as))
(non (privk c)))
(exists ((z-0 strd))
(and (p "auth" z-0 2) (p "auth" "as" z-0 as)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c))))))
(label 8)
(unrealized (0 1))
(origs (n1 (0 0)) (n2 (0 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k9">Item <a href="#t8">9</a>, Parent: <a href="#k8">8</a>, Children: <a href="#k10">10</a> <a href="#k11">11</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>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</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>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 9</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c as t name)
(k ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c)
(t t) (as as) (k k) (ak ak-0))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak-0)
(operation encryption-test (added-strand auth 2)
(enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (0 1))
(label 9)
(parent 8)
(unrealized (0 1))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k10">Item <a href="#t8">10</a>, Parent: <a href="#k9">9</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>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</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>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 10 (realized)</text></svg>
</div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tgt tk tgt-0 data) (c as t name) (k ak skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
(t t) (as as) (k k) (ak ak))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (displaced 2 1 auth 2)
(enc ak-0 n1 tk-0 t k) (0 1))
(label 10)
(parent 9)
(unrealized)
(shape)
(satisfies yes)
(maps
((0)
((c c) (as as) (k k) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk)
(tgt tgt) (ak ak))))
(origs (k (1 1)) (ak (1 1)) (n1 (0 0)) (n2 (0 0))))</pre>
<p id="k11">Item <a href="#t8">11</a>, Parent: <a href="#k9">9</a>, Child: <a href="#k12">12</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='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='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 45.960 264.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>k</title><circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>k</title>
<circle style='fill: red;' 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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 11</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c as t name)
(k ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c)
(t t) (as as) (k k) (ak ak-0))
(deflistener k)
(precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak-0)
(operation encryption-test (added-listener k) (enc ak n1 tk t k)
(0 1))
(label 11)
(parent 9)
(unrealized (2 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k12">Item <a href="#t8">12</a>, Parent: <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='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='114.960' x2='39.960' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<path
d='M 239.880 264.960 Q 142.920 227.460 45.960 264.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>ak-0</title><circle cx='239.880' cy='264.960' r='6.000'/>
</g>
<g><title>ak-0</title>
<circle style='fill: red;' 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-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc ak-0 (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t ak-0))</title>
<circle cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc ak-0 (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak-0))</title>
<circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
<path
d='M 39.960 114.960 Q 86.940 114.960 133.920 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k ak-0) (ak ak-0))</title>
<text x='139.920' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak-0) (ak ak))</title>
<text
x='39.960' y='77.460' style='text-anchor: middle;'>client</text></g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 12</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c as t name)
(ak ak-0 skey))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k ak-0) (ak ak))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c)
(t t) (as as) (k ak-0) (ak ak-0))
(deflistener ak-0)
(precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 ak-0)
(operation nonce-test (displaced 3 1 auth 2) k (2 0)
(enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
(pubk c)))
(label 12)
(parent 11)
(unrealized (2 0))
(comment "empty cohort"))</pre>
<p id="t13">Tree <a href="#top">13</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("#k15", "_self")'>15</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("#k14", "_self")'>14</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("#k13", "_self")'>13</text>
</svg></div>
<pre>(defprotocol pkinit-flawed basic
(defrole client
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (send (cat (enc tc n2 (privk c)) c t n1))
(recv
(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig n2 n1))
(defrole auth
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (recv (cat (enc tc n2 (privk c)) c t n1))
(send
(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig k ak)))</pre>
<p id="k13">Item <a href="#t13">13</a>, Child: <a href="#k14">14</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>(cat (enc (enc k n2-0 (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-flawed 13</text></svg></div>
<pre>(defskeleton pkinit-flawed
(vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as-0) (k k) (ak ak))
(defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
(tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
(non-orig (privk c) (privk as))
(uniq-orig n2-0 n1-0 k ak)
(goals
(forall ((c c-0 as name) (k skey) (z z-0 strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (p "auth" z-0 2)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
(non (privk c))) (= c c-0))))
(label 13)
(unrealized (1 1))
(origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
(preskeleton)
(comment "Not a skeleton"))</pre>
<p id="k14">Item <a href="#t13">14</a>, Parent: <a href="#k13">13</a>, Child: <a href="#k15">15</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>(cat (enc (enc k n2-0 (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-flawed 14</text></svg></div>
<pre>(defskeleton pkinit-flawed
(vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as-0) (k k) (ak ak))
(defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
(tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2-0 n1-0 k ak)
(goals
(forall ((c c-0 as name) (k skey) (z z-0 strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (p "auth" z-0 2)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
(non (privk c))) (= c c-0))))
(label 14)
(parent 13)
(unrealized (1 1))
(origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k15">Item <a href="#t13">15</a>, Parent: <a href="#k14">14</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>(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</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>(cat (enc tc-0 n2 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 (privk as)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-flawed 15 (realized)</text></svg>
</div>
<pre>(defskeleton pkinit-flawed
(vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 t as t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 1) (1 1)) ((1 0) (0 0)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1-0 k ak)
(operation encryption-test (displaced 2 0 auth 2)
(enc k n2-0 (privk as-0)) (1 1))
(label 15)
(parent 14)
(unrealized)
(shape)
(satisfies (no (c c) (c-0 c-0) (as as) (k k) (z 1) (z-0 0)))
(maps
((0 1)
((c c) (c-0 c-0) (as as) (k k) (t t) (as-0 as) (n2 n2) (n1 n1)
(tc tc) (tk tk) (tgt tgt) (ak ak) (t-0 t-0) (n2-0 n2)
(n1-0 n1-0) (tc-0 tc-0) (tk-0 tk-0) (tgt-0 tgt-0) (ak-0 ak-0))))
(origs (k (0 1)) (ak (0 1)) (n1-0 (1 0)) (n2 (1 0))))</pre>
<p id="t16">Tree <a href="#top">16</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='text-anchor: middle; fill: red;'
onclick='window.open("#k22", "_self")'>22</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: red;'
onclick='window.open("#k20", "_self")'>20</text>
<line
x1='139.800' y1='77.460' x2='189.720' y2='114.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='239.640' y='26.040'
style='font-weight: bold; text-anchor: middle; fill: blue;'
onclick='window.open("#k21", "_self")'>21</text>
<line
x1='189.720' y1='39.960' x2='239.640' y2='39.960'
style='stroke-width: 0.960; stroke: gray;'/>
<text
x='189.720' y='26.040' style='text-anchor: middle; fill: black;'
onclick='window.open("#k19", "_self")'>19</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("#k18", "_self")'>18</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("#k17", "_self")'>17</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("#k16", "_self")'>16</text>
</svg></div>
<pre>(defprotocol pkinit-fix1 basic
(defrole client
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (send (cat (enc tc n2 (privk c)) c t n1))
(recv
(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig n2 n1))
(defrole auth
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (recv (cat (enc tc n2 (privk c)) c t n1))
(send
(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
(enc ak n1 tk t k))))
(uniq-orig k ak)))</pre>
<p id="k16">Item <a href="#t16">16</a>, Child: <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;'/>
<g>
<title>(cat (enc (enc k n2-0 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 c-0 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 16</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as-0) (k k) (ak ak))
(defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
(tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
(non-orig (privk c) (privk as))
(uniq-orig n2-0 n1-0 k ak)
(goals
(forall ((c c-0 as name) (k skey) (z z-0 strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (p "auth" z-0 2)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
(non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2)))))
(label 16)
(unrealized (1 1))
(origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
(preskeleton)
(comment "Not a skeleton"))</pre>
<p id="k17">Item <a href="#t16">17</a>, Parent: <a href="#k16">16</a>, Child: <a href="#k18">18</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>(cat (enc (enc k n2-0 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 c-0 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 17</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as-0) (k k) (ak ak))
(defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
(tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2-0 n1-0 k ak)
(goals
(forall ((c c-0 as name) (k skey) (z z-0 strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (p "auth" z-0 2)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
(non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2)))))
(label 17)
(parent 16)
(unrealized (1 1))
(origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k18">Item <a href="#t16">18</a>, Parent: <a href="#k17">17</a>, Children: <a href="#k19">19</a> <a href="#k20">20</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>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</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>(cat (enc tc-0 n2 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 18</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c t as t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 1) (1 1)) ((1 0) (0 0)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1-0 k ak)
(operation encryption-test (displaced 2 0 auth 2)
(enc k n2-0 c-0 (privk as-0)) (1 1))
(label 18)
(parent 17)
(unrealized (0 0) (1 1))
(origs (k (0 1)) (ak (0 1)) (n1-0 (1 0)) (n2 (1 0)))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k19">Item <a href="#t16">19</a>, Parent: <a href="#k18">18</a>, Child: <a href="#k21">21</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>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k))</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>(cat (enc tc-0 n2 (privk c)) c t n1)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc-0) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 19</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 text) (tc tk tgt tc-0 tgt-0 data) (c t as name)
(k ak skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc-0) (tk tk) (tgt tgt-0)
(c c) (t t) (as as) (k k) (ak ak))
(precedes ((0 1) (1 1)) ((1 0) (0 0)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (displaced 2 0 auth 2)
(enc ak-0 n1-0 tk-0 t-0 k) (1 1))
(label 19)
(parent 18)
(unrealized (0 0))
(origs (k (0 1)) (ak (0 1)) (n1 (1 0)) (n2 (1 0)))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k20">Item <a href="#t16">20</a>, Parent: <a href="#k18">18</a>, Child: <a href="#k22">22</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='189.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='114.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='189.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>k</title><circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>k</title>
<circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc-0 n2 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 136.920 152.460 233.880 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 20</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c t as t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k k) (ak ak-0))
(deflistener k)
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1-0 k ak)
(operation encryption-test (added-listener k)
(enc ak-0 n1-0 tk-0 t-0 k) (1 1))
(label 20)
(parent 18)
(unrealized (0 0) (2 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k21">Item <a href="#t16">21</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;'/>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k))</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>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 21 (realized)</text></svg>
</div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 text) (tk tgt tc tgt-0 data) (c t as name) (k ak skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
(t t) (as as) (k k) (ak ak))
(precedes ((0 1) (1 1)) ((1 0) (0 0)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (displaced 2 1 client 1)
(enc tc-0 n2 (privk c)) (0 0))
(label 21)
(parent 19)
(unrealized)
(shape)
(satisfies yes)
(maps
((0 1)
((c c) (c-0 c) (as as) (k k) (t t) (as-0 as) (n2 n2) (n1 n1)
(tc tc) (tk tk) (tgt tgt) (ak ak) (t-0 t) (n2-0 n2) (n1-0 n1)
(tc-0 tc) (tk-0 tk) (tgt-0 tgt-0) (ak-0 ak))))
(origs (n1 (1 0)) (n2 (1 0)) (k (0 1)) (ak (0 1))))</pre>
<p id="k22">Item <a href="#t16">22</a>, Parent: <a href="#k20">20</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='189.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='114.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='189.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>ak</title><circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>ak</title>
<circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc ak n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 ak))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc-0 n2 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 136.920 152.460 233.880 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc ak n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k ak) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix1 22</text></svg></div>
<pre>(defskeleton pkinit-fix1
(vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c t as t-0 name) (ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k ak) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
(c c) (t t-0) (as as) (k ak) (ak ak-0))
(deflistener ak)
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1-0 ak)
(operation nonce-test (displaced 3 0 auth 2) k (2 0)
(enc (enc k n2 c (privk as)) (pubk c)))
(label 22)
(parent 20)
(unrealized (0 0) (2 0))
(comment "empty cohort"))</pre>
<p id="t23">Tree <a href="#top">23</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='text-anchor: middle; fill: red;'
onclick='window.open("#k28", "_self")'>28</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: red;'
onclick='window.open("#k27", "_self")'>27</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("#k26", "_self")'>26</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("#k25", "_self")'>25</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("#k24", "_self")'>24</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("#k23", "_self")'>23</text>
</svg></div>
<pre>(defprotocol pkinit-fix2 basic
(defrole client
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (send (cat (enc tc n2 (privk c)) c t n1))
(recv
(cat
(enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
(pubk c)) c tgt (enc ak n1 tk t k))))
(uniq-orig n2 n1))
(defrole auth
(vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
(trace (recv (cat (enc tc n2 (privk c)) c t n1))
(send
(cat
(enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
(pubk c)) c tgt (enc ak n1 tk t k))))
(uniq-orig k ak)))</pre>
<p id="k23">Item <a href="#t23">23</a>, Child: <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;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c-0)) c-0 t n1) (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 23</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as-0) (k k) (ak ak))
(defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
(tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
(non-orig (privk c) (privk as))
(uniq-orig n2-0 n1-0 k ak)
(goals
(forall ((c c-0 as name) (k skey) (z z-0 strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (p "auth" z-0 2)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
(non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2)))))
(label 23)
(unrealized (1 1))
(origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
(preskeleton)
(comment "Not a skeleton"))</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;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c-0)) c-0 t n1) (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c-0)) c-0 t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 24</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
(c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
(t t) (as as-0) (k k) (ak ak))
(defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
(tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
(precedes ((0 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2-0 n1-0 k ak)
(goals
(forall ((c c-0 as name) (k skey) (z z-0 strd))
(implies
(and (p "client" z 2) (p "client" "c" z c)
(p "client" "as" z as) (p "client" "k" z k) (p "auth" z-0 2)
(p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
(non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2)))))
(label 24)
(parent 23)
(unrealized (1 1))
(origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (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>, Children: <a href="#k26">26</a> <a href="#k27">27</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>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k))</title>
<circle style='fill: red;' cx='139.920' cy='189.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 25</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c t as name)
(k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0)
(c c) (t t) (as as) (k k) (ak ak-0))
(precedes ((0 1) (1 1)) ((1 0) (0 0)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (displaced 2 0 auth 2)
(enc k (hash (enc tc-0 n2-0 (privk c-0)) c-0 t-0 n1-0) (privk as-0))
(1 1))
(label 25)
(parent 24)
(unrealized (1 1))
(origs (k (0 1)) (ak (0 1)) (n1 (1 0)) (n2 (1 0)))
(comment "2 in cohort - 2 not yet seen"))</pre>
<p id="k26">Item <a href="#t23">26</a>, Parent: <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;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k))</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>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='89.940' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 26 (realized)</text></svg>
</div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tgt-0 data) (c t as name) (k ak skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
(t t) (as as) (k k) (ak ak))
(precedes ((0 1) (1 1)) ((1 0) (0 0)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (displaced 2 0 auth 2)
(enc ak-0 n1 tk-0 t k) (1 1))
(label 26)
(parent 25)
(unrealized)
(shape)
(satisfies yes)
(maps
((0 1)
((c c) (c-0 c) (as as) (k k) (t t) (as-0 as) (n2 n2) (n1 n1)
(tc tc) (tk tk) (tgt tgt) (ak ak) (t-0 t) (n2-0 n2) (n1-0 n1)
(tc-0 tc) (tk-0 tk) (tgt-0 tgt-0) (ak-0 ak))))
(origs (k (0 1)) (ak (0 1)) (n1 (1 0)) (n2 (1 0))))</pre>
<p id="k27">Item <a href="#t23">27</a>, Parent: <a href="#k25">25</a>, Child: <a href="#k28">28</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='189.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='114.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='189.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>k</title><circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>k</title>
<circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 136.920 152.460 233.880 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 27</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c t as name)
(k ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k k) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0)
(c c) (t t) (as as) (k k) (ak ak-0))
(deflistener k)
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 k ak)
(operation encryption-test (added-listener k) (enc ak-0 n1 tk-0 t k)
(1 1))
(label 27)
(parent 25)
(unrealized (2 0))
(comment "1 in cohort - 1 not yet seen"))</pre>
<p id="k28">Item <a href="#t23">28</a>, Parent: <a href="#k27">27</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='189.960' x2='239.880' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='139.920' y1='114.960' x2='139.920' y2='264.960'
style='stroke-width: 0.960; stroke: gray;'/>
<line
x1='39.960' y1='114.960' x2='39.960' y2='189.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>ak</title><circle cx='239.880' cy='264.960' r='6.000'/></g>
<g><title>ak</title>
<circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
<g>
<title>(cat (enc (enc ak (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t ak))</title>
<circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
<path
d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'
style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle cx='139.920' cy='114.960' r='6.000'/></g>
<path
d='M 39.960 189.960 Q 136.920 152.460 233.880 189.960'
style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
<g>
<title>(cat (enc (enc ak (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak))</title>
<circle cx='39.960' cy='189.960' r='6.000'/></g>
<g><title>(cat (enc tc n2 (privk c)) c t n1)</title>
<circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k ak) (ak ak-0))</title>
<text
x='139.920' y='77.460' style='text-anchor: middle;'>client</text>
</g>
<g>
<title>((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak) (ak ak))</title>
<text x='39.960' y='77.460' style='text-anchor: middle;'>auth</text>
</g>
<text
x='139.920' y='39.960'
style='text-anchor: middle;'>pkinit-fix2 28</text></svg></div>
<pre>(defskeleton pkinit-fix2
(vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c t as name)
(ak ak-0 skey))
(defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
(t t) (as as) (k ak) (ak ak))
(defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0)
(c c) (t t) (as as) (k ak) (ak ak-0))
(deflistener ak)
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
(non-orig (privk c) (privk as))
(uniq-orig n2 n1 ak)
(operation nonce-test (displaced 3 0 auth 2) k (2 0)
(enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
(pubk c)))
(label 28)
(parent 27)
(unrealized (2 0))
(comment "empty cohort"))</pre>
</body>
</html>