---

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

---

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

---

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


Date html generated: 2010_08_28-AM-11_47_35
Last ObjectModification: 2010_03_15-PM-09_18_43

Home Index