fnof_yahalom.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.6.2 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function</title>
 <meta http-equiv="content-type" content="application/xhtml+xml; charset=UTF-8" />
 <style>
  svg.diagram { border-width: 1px; border-style: solid }
 </style>
</head>
<body>

<pre>(herald
  &quot;Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function&quot;
  (bound 12))
(comment &quot;CPSA 3.6.2&quot;)
(comment &quot;All input read from fnof_yahalom.scm&quot;)</pre>

<p id="top">Trees: <a href="#t0">0</a> <a href="#t4">4</a> <a href="#t10">10</a> <a href="#t15">15</a>.</p>

<p id="t0">Tree <a href="#top">0</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(&quot;#k3&quot;, &quot;_self&quot;)'>3</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(&quot;#k2&quot;, &quot;_self&quot;)'>2</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(&quot;#k1&quot;, &quot;_self&quot;)'>1</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(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (ltkac k skey))
    (trace (init (cat c ltkac)) (send (cat a n-a))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k)))
    (fn-of (&quot;ltk&quot; (ltkac (cat a c))) (&quot;ltk-inv&quot; ((cat a c) ltkac))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init (cat c ltkac)) (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc))) (recv (enc a k ltkbc))
      (recv (enc n-b k)))
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
      (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init c) (recv (cat b (enc a n-a n-b ltkbc)))
      (send (enc b k n-a n-b ltkac)) (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
      (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))))</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='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 0</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
    (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b)
  (label 0)
  (unrealized (0 3))
  (origs (n-b (0 2)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

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

<pre>(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (precedes ((1 3) (0 3)))
  (fn-of (&quot;ltk&quot; (ltkbc (cat b c)) (ltkac (cat a c)))
    (&quot;ltk-inv&quot; ((cat b c) ltkbc) ((cat a c) ltkac)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 4) (enc a k ltkbc)
    (0 3))
  (label 1)
  (parent 0)
  (unrealized (1 1))
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k2">Item <a href="#t0">2</a>, Parent: <a href="#k1">1</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='189.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>(enc b k n-a n-b ltkac)</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.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>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 2 (realized)</text></svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 4 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (precedes ((0 2) (1 1)) ((1 3) (0 3)))
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
    (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 2 0 resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (1 1))
  (label 2)
  (parent 1)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k (1 2)) (n-b (0 2))))</pre>

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

<div>
 <svg
  class='diagram' width='279.840pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='239.880' y1='114.960' x2='239.880' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='189.960' x2='39.960' y2='414.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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a-0)</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='239.880' cy='114.960' r='6.000'/></g>
  <path
   d='M 139.920 414.960 Q 92.940 414.960 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>(enc b k n-a-0 n-b-0 ltkac)</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 3 (realized)</text></svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (defstrand resp 3 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)
    (ltkac ltkac) (ltkbc ltkbc))
  (precedes ((1 3) (0 3)) ((2 2) (1 1)))
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
    (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (1 1))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k (1 2)) (n-b (0 2))))</pre>

<p id="t4">Tree <a href="#top">4</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(&quot;#k9&quot;, &quot;_self&quot;)'>9</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(&quot;#k7&quot;, &quot;_self&quot;)'>7</text>
  <line
   x1='89.880' y1='77.460' x2='139.800' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='26.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k8&quot;, &quot;_self&quot;)'>8</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: red;'
   onclick='window.open(&quot;#k6&quot;, &quot;_self&quot;)'>6</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: red;'
   onclick='window.open(&quot;#k5&quot;, &quot;_self&quot;)'>5</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: red;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  </svg></div>

<pre>(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (ltkac k skey))
    (trace (init (cat c ltkac)) (send (cat a n-a))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k)))
    (fn-of (&quot;ltk&quot; (ltkac (cat a c))) (&quot;ltk-inv&quot; ((cat a c) ltkac))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init (cat c ltkac)) (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc))) (recv (enc a k ltkbc))
      (recv (enc n-b k)))
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
      (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (init c) (recv (cat b (enc a n-a n-b ltkbc)))
      (send (enc b k n-a n-b ltkac)) (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
      (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))))</pre>

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

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>k</title><circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 4</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
    (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b)
  (label 4)
  (unrealized (0 3))
  (origs (n-b (0 2)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k5">Item <a href="#t4">5</a>, Parent: <a href="#k4">4</a>, Children: <a href="#k6">6</a> <a href="#k7">7</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='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='264.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 339.960 Q 142.920 302.460 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='339.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 b k n-a-0 n-b-0 ltkac)</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: red;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='239.880' cy='114.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: red;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 5</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (precedes ((2 2) (1 0)) ((2 3) (0 3)))
  (fn-of (&quot;ltk&quot; (ltkbc (cat b c)) (ltkac (cat a c)))
    (&quot;ltk-inv&quot; ((cat b c) ltkbc) ((cat a c) ltkac)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 4) (enc a k ltkbc)
    (0 3))
  (label 5)
  (parent 4)
  (unrealized (1 0) (2 1))
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k6">Item <a href="#t4">6</a>, Parent: <a href="#k5">5</a>, Child: <a href="#k8">8</a>.</p>

<div>
 <svg
  class='diagram' width='279.840pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='339.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 414.960 Q 142.920 377.460 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='414.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc b k n-a n-b ltkac)</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: red;' cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 136.920 227.460 233.880 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 6</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (precedes ((0 2) (2 1)) ((2 2) (1 0)) ((2 3) (0 3)))
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
    (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 3 0 resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (2 1))
  (label 6)
  (parent 5)
  (unrealized (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k7">Item <a href="#t4">7</a>, Parent: <a href="#k5">5</a>, Child: <a href="#k9">9</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='339.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='189.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a-0)</title>
   <circle style='fill: blue;' cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 414.960 Q 142.920 377.460 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='414.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc b k n-a-0 n-b-0 ltkac)</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: red;' cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960' style='text-anchor: middle;'>yahalom 7</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (defstrand resp 3 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)
    (ltkac ltkac) (ltkbc ltkbc))
  (precedes ((2 2) (1 0)) ((2 3) (0 3)) ((3 2) (2 1)))
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))
    (&quot;ltk-inv&quot; ((cat a c) ltkac) ((cat b c) ltkbc)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 3)
    (enc a n-a-0 n-b-0 ltkbc) (2 1))
  (label 7)
  (parent 5)
  (unrealized (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k8">Item <a href="#t4">8</a>, Parent: <a href="#k6">6</a>.</p>

<div>
 <svg
  class='diagram' width='279.840pt' height='529.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 529.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='414.960' x2='139.920' y2='489.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 414.960 Q 142.920 377.460 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <path
   d='M 239.880 414.960 Q 192.900 414.960 145.920 414.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='414.960' r='6.000'/></g>
  <g><title>(enc b k n-a n-b ltkac)</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='489.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: red;' cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 136.920 227.460 233.880 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom 8</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a) (n-b n-b) (c c) (a a) (b b) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (precedes ((0 2) (2 1)) ((2 3) (0 3)) ((2 3) (1 0)))
  (fn-of (&quot;ltk&quot; (ltkbc (cat b c)) (ltkac (cat a c)))
    (&quot;ltk-inv&quot; ((cat b c) ltkbc) ((cat a c) ltkac)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation nonce-test (displaced 3 2 serv 4) k (1 0)
    (enc b k n-a n-b ltkac))
  (label 8)
  (parent 6)
  (unrealized (1 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="k9">Item <a href="#t4">9</a>, Parent: <a href="#k7">7</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='529.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 529.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='414.960' x2='139.920' y2='489.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='189.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 292.860 264.960 245.880 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a-0)</title>
   <circle style='fill: blue;' cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 414.960 Q 142.920 377.460 45.960 414.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <path
   d='M 239.880 414.960 Q 192.900 414.960 145.920 414.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='414.960' r='6.000'/></g>
  <g><title>(enc b k n-a-0 n-b-0 ltkac)</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>c</title>
   <circle style='fill: gray;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='489.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: red;' cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc))</title>
   <circle cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat c ltkac)</title>
   <circle style='fill: gray;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960' style='text-anchor: middle;'>yahalom 9</text>
  </svg></div>

<pre>(defskeleton yahalom
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 4 (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b)
    (ltkac ltkac) (ltkbc ltkbc) (k k))
  (defstrand resp 3 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c)
    (ltkac ltkac) (ltkbc ltkbc))
  (precedes ((2 3) (0 3)) ((2 3) (1 0)) ((3 2) (2 1)))
  (fn-of (&quot;ltk&quot; (ltkbc (cat b c)) (ltkac (cat a c)))
    (&quot;ltk-inv&quot; ((cat b c) ltkbc) ((cat a c) ltkac)))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation nonce-test (displaced 4 2 serv 4) k (1 0)
    (enc b k n-a-0 n-b-0 ltkac))
  (label 9)
  (parent 7)
  (unrealized (1 0))
  (comment &quot;empty cohort&quot;))</pre>

<p id="t10">Tree <a href="#top">10</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(&quot;#k14&quot;, &quot;_self&quot;)'>14</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(&quot;#k13&quot;, &quot;_self&quot;)'>13</text>
  <line
   x1='89.880' y1='77.460' x2='139.800' y2='114.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k12&quot;, &quot;_self&quot;)'>12</text>
  <line
   x1='89.880' y1='77.460' x2='139.800' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='63.540' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k11&quot;, &quot;_self&quot;)'>11</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(&quot;#k10&quot;, &quot;_self&quot;)'>10</text>
  </svg></div>

<pre>(defprotocol yahalom2 basic
  (defrole init
    (vars (a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (send (cat a n-a (hash ltkbc)))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc) (hash c ltkac)))
      (recv (enc a k ltkbc)) (recv (enc n-b k)))
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat b (enc a n-a n-b ltkbc)))
      (send (cat (hash c) (enc b k n-a n-b ltkac)))
      (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c))))))</pre>

<p id="k10">Item <a href="#t10">10</a>, Child: <a href="#k11">11</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n-b k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 10</text>
  </svg></div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b)
  (label 10)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k11">Item <a href="#t10">11</a>, Parent: <a href="#k10">10</a>, Children: <a href="#k12">12</a> <a href="#k13">13</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 139.920 264.960 Q 92.940 264.960 45.960 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0))</title>
   <circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: red;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 11</text>
  </svg></div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((1 2) (0 2)))
  (fn-of
    (&quot;ltk&quot; (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 3) (enc a k ltkbc)
    (0 2))
  (label 11)
  (parent 10)
  (unrealized (0 3) (1 0))
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k12">Item <a href="#t10">12</a>, Parent: <a href="#k11">11</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='189.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 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 a k ltkbc)</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat (hash c-0) (enc b-0 k n-a n-b ltkac-0))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 86.940 189.960 133.920 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 12 (realized)</text></svg>
 </div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)))
  (fn-of
    (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (1 0))
  (label 12)
  (parent 11)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k (1 1)) (n-b (0 1))))</pre>

<p id="k13">Item <a href="#t10">13</a>, Parent: <a href="#k11">11</a>, Child: <a href="#k14">14</a>.</p>

<div>
 <svg
  class='diagram' width='279.840pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='239.880' y1='114.960' x2='239.880' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='189.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a-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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: red;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 13</text></svg></div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (precedes ((1 2) (0 2)) ((2 1) (1 0)))
  (fn-of
    (&quot;ltk&quot; (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1))
      (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (1 0))
  (label 13)
  (parent 11)
  (unrealized (0 3))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='339.840' y1='189.960' x2='339.840' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='114.960' x2='239.880' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='189.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 264.960 Q 192.583 301.118 45.326 412.276'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (hash c-2) (enc b-2 k-0 n-a n-b ltkac-2))</title>
   <circle cx='339.840' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-2 (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='339.840' cy='189.960' r='6.000'/></g>
  <path
   d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a-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-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0))</title>
   <circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 186.900 152.460 333.840 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2) (ltkac ltkac-2) (ltkbc ltkbc) (k k-0))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='139.920' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>yahalom2 14 (realized)</text></svg>
 </div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 c-2 b-2 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 ltkac-2 k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2)
    (ltkac ltkac-2) (ltkbc ltkbc) (k k-0))
  (precedes ((0 1) (3 0)) ((1 2) (0 2)) ((2 1) (1 0)) ((3 1) (0 3)))
  (fn-of
    (&quot;ltk&quot; (ltkac-2 (cat a c-2)) (ltkbc (cat b-2 c-2))
      (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0)) (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 2) n-b (0 3)
    (enc a n-a n-b ltkbc))
  (label 14)
  (parent 13)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (n-a n-a)
        (k k))))
  (origs (k-0 (3 1)) (k (1 1)) (n-b (0 1))))</pre>

<p id="t15">Tree <a href="#top">15</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(&quot;#k19&quot;, &quot;_self&quot;)'>19</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(&quot;#k18&quot;, &quot;_self&quot;)'>18</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(&quot;#k17&quot;, &quot;_self&quot;)'>17</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(&quot;#k16&quot;, &quot;_self&quot;)'>16</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(&quot;#k15&quot;, &quot;_self&quot;)'>15</text>
  </svg></div>

<pre>(defprotocol yahalom2 basic
  (defrole init
    (vars (a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (send (cat a n-a (hash ltkbc)))
      (recv (enc b k n-a n-b ltkac)) (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat a n-a))
      (send (cat b (enc a n-a n-b ltkbc) (hash c ltkac)))
      (recv (enc a k ltkbc)) (recv (enc n-b k)))
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (ltkac ltkbc k skey))
    (trace (recv (cat b (enc a n-a n-b ltkbc)))
      (send (cat (hash c) (enc b k n-a n-b ltkac)))
      (send (enc a k ltkbc)))
    (uniq-orig k)
    (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c))))))</pre>

<p id="k15">Item <a href="#t15">15</a>, Child: <a href="#k16">16</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>k</title><circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: blue;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 15</text>
  </svg></div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a text) (a b c name) (ltkac ltkbc k skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (fn-of (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b)
  (label 15)
  (unrealized (0 2) (0 3))
  (origs (n-b (0 1)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k16">Item <a href="#t15">16</a>, Parent: <a href="#k15">15</a>, Children: <a href="#k17">17</a> <a href="#k18">18</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='189.960' x2='139.920' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 264.960 Q 142.920 227.460 45.960 264.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 239.880 189.960 Q 192.900 189.960 145.920 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0))</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: red;' cx='239.880' cy='114.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: blue;' cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 16</text></svg></div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)))
  (fn-of
    (&quot;ltk&quot; (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand serv 3) (enc a k ltkbc)
    (0 2))
  (label 16)
  (parent 15)
  (unrealized (0 3) (2 0))
  (comment &quot;2 in cohort - 2 not yet seen&quot;))</pre>

<p id="k17">Item <a href="#t15">17</a>, Parent: <a href="#k16">16</a>.</p>

<div>
 <svg
  class='diagram' width='279.840pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='264.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 339.960 Q 142.920 302.460 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='339.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>(cat (hash c-0) (enc b-0 k n-a n-b ltkac-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 136.920 152.460 233.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</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;'>yahalom2 17 (realized)</text></svg>
 </div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a text) (a b c c-0 b-0 name)
    (ltkac ltkbc k ltkac-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a) (n-b n-b) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)) ((2 2) (0 2)))
  (fn-of
    (&quot;ltk&quot; (ltkac (cat a c)) (ltkbc (cat b c)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (2 0))
  (label 17)
  (parent 16)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (k k)
        (n-a n-a))))
  (origs (k (2 1)) (n-b (0 1))))</pre>

<p id="k18">Item <a href="#t15">18</a>, Parent: <a href="#k16">16</a>, Child: <a href="#k19">19</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='264.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='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1))</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a-0)</title>
   <circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 142.920 302.460 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='339.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>(cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: red;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>yahalom2 18</text></svg></div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0)))
  (fn-of
    (&quot;ltk&quot; (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1))
      (ltkac-0 (cat a c-0)) (ltkbc (cat b-0 c-0)) (ltkac (cat a c))
      (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 ltkbc) (2 0))
  (label 18)
  (parent 16)
  (unrealized (0 3))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k19">Item <a href="#t15">19</a>, Parent: <a href="#k18">18</a>.</p>

<div>
 <svg
  class='diagram' width='479.760pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 479.760 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='439.800' y1='189.960' x2='439.800' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='189.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='264.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 439.800 264.960 Q 242.689 301.406 45.578 412.852'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat (hash c-2) (enc b-2 k-0 n-a n-b ltkac-2))</title>
   <circle cx='439.800' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-2 (enc a n-a n-b ltkbc))</title>
   <circle style='fill: blue;' cx='439.800' cy='189.960' r='6.000'/></g>
  <path
   d='M 339.840 189.960 Q 292.860 189.960 245.880 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g>
   <title>(cat b-1 (enc a n-a-0 n-b-0 ltkbc) (hash c-1 ltkac-1))</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a-0)</title>
   <circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 142.920 302.460 45.960 339.960'
   style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(enc a k ltkbc)</title>
   <circle cx='239.880' cy='339.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>(cat (hash c-0) (enc b-0 k n-a-0 n-b-0 ltkac-0))</title>
   <circle cx='239.880' cy='264.960' r='6.000'/></g>
  <g><title>(cat b-0 (enc a n-a-0 n-b-0 ltkbc))</title>
   <circle style='fill: blue;' cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>k</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>k</title>
   <circle style='fill: blue;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(enc n-b k)</title>
   <circle style='fill: blue;' cx='39.960' cy='414.960' r='6.000'/></g>
  <g><title>(enc a k ltkbc)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 189.960 Q 236.880 152.460 433.800 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b (enc a n-a n-b ltkbc) (hash c ltkac))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat a n-a)</title>
   <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>
  <g>
   <title>((n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2) (ltkac ltkac-2) (ltkbc ltkbc) (k k-0))</title>
   <text x='439.800' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1) (ltkac ltkac-1) (ltkbc ltkbc))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g>
   <title>((n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0) (ltkac ltkac-0) (ltkbc ltkbc) (k k))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>serv</text>
   </g>
  <g>
   <title>((n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac) (ltkbc ltkbc) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <text
   x='239.880' y='39.960'
   style='text-anchor: middle;'>yahalom2 19 (realized)</text></svg>
 </div>

<pre>(defskeleton yahalom2
  (vars (n-b n-a n-a-0 n-b-0 text) (a b c c-0 b-0 b-1 c-1 c-2 b-2 name)
    (ltkac ltkbc k ltkac-0 ltkac-1 ltkac-2 k-0 skey))
  (defstrand resp 4 (n-a n-a) (n-b n-b) (b b) (a a) (c c) (ltkac ltkac)
    (ltkbc ltkbc) (k k))
  (deflistener k)
  (defstrand serv 3 (n-a n-a-0) (n-b n-b-0) (c c-0) (a a) (b b-0)
    (ltkac ltkac-0) (ltkbc ltkbc) (k k))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b-1) (a a) (c c-1)
    (ltkac ltkac-1) (ltkbc ltkbc))
  (defstrand serv 2 (n-a n-a) (n-b n-b) (c c-2) (a a) (b b-2)
    (ltkac ltkac-2) (ltkbc ltkbc) (k k-0))
  (precedes ((0 1) (4 0)) ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0))
    ((4 1) (0 3)))
  (fn-of
    (&quot;ltk&quot; (ltkac-2 (cat a c-2)) (ltkbc (cat b-2 c-2))
      (ltkac-1 (cat a c-1)) (ltkbc (cat b-1 c-1)) (ltkac-0 (cat a c-0))
      (ltkbc (cat b-0 c-0)) (ltkac (cat a c)) (ltkbc (cat b c))))
  (non-orig ltkac ltkbc)
  (uniq-orig n-b k k-0)
  (operation nonce-test (added-strand serv 2) n-b (0 3)
    (enc a n-a n-b ltkbc))
  (label 19)
  (parent 18)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((a a) (b b) (c c) (n-b n-b) (ltkac ltkac) (ltkbc ltkbc) (k k)
        (n-a n-a))))
  (origs (k-0 (4 1)) (k (2 1)) (n-b (0 1))))</pre>

</body>
</html>