---

CR-initiator3 ==
  A  B: (["new"(m); "send"(data(m))] @ ["rcv"(<data(n), data(s)>)])
          @ ["verify"(<<data(n), <data(A), data(m)>>, B, s>); 
             
             "sign"(<<data(m), <data(B), data(n)>>, A, s'>); "send"(data(s'))]

---

Definitions :  basic-seq-1-5: A  B: pas[A;B;m;n;x;y;z],  append: as @ bs,  sdata-pair: <d1, d2>,  id-sdata: data(x),  pair: <a, b>,  cons: [car / cdr],  mk-pa: n(v),  token: "$token",  atom-sdata: data(a),  nil: []
FDL editor aliases :  CR-initiator3

---

CR-initiator3  ==
    A  {}\mrightarrow{}  B:  (["new"(m);  "send"(data(m))]  @  ["rcv"(<data(n),  data(s)>)])
                    @  ["verify"(<<data(n),  <data(A),  data(m)>>,  B,  s>); 
                         
                          "sign"(<<data(m),  <data(B),  data(n)>>,  A,  s'>);  "send"(data(s'))]


Date html generated: 2010_08_28-AM-11_47_18
Last ObjectModification: 2010_03_16-PM-05_11_02

Home Index