plaindh.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.6.2 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Plain diffie-hellman protocol with challenge-response</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;Plain diffie-hellman protocol with challenge-response&quot;
  (algebra diffie-hellman))
(comment &quot;CPSA 3.6.2&quot;)
(comment &quot;All input read from plaindh.scm&quot;)</pre>

<p id="t0">Tree 0.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 79.920' font-size='12.000'>
  <text
   x='39.960' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol plaindh diffie-hellman
  (defrole init
    (vars (x rndx) (y expt) (n text))
    (trace (send (exp (gen) x)) (recv (exp (gen) y))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    (uniq-orig n)
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (x expt) (n text))
    (trace (recv (exp (gen) x)) (send (exp (gen) y))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    (uniq-gen y)
    (absent (y (exp (gen) x))))
  (comment &quot;Diffie-hellman key exchange followed by an encryption&quot;))</pre>

<p id="k0">Item <a href="#t0">0</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>n</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n (exp (gen) (mul x y)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(exp (gen) y)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(exp (gen) x)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n n) (x x) (y y))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960'
   style='text-anchor: middle;'>plaindh 0 (realized)</text></svg></div>

<pre>(defskeleton plaindh
  (vars (n text) (x rndx) (y expt))
  (defstrand init 4 (n n) (x x) (y y))
  (uniq-gen x)
  (uniq-orig n)
  (label 0)
  (unrealized)
  (shape)
  (maps ((0) ((x x) (y y) (n n))))
  (origs (n (0 2))))</pre>

</body>
</html>