Nuprl Definition : NSL-responder3

NSL-responder3 ==
  B ─→ A: (["rcv"(data(c));
            "decrypt"(<<data(m), data(A)>PrivateKey(B), c>);
            "new"(n);
            "encrypt"(<<data(m), <data(n), data(B)>>PublicKey(A), c'>);
            "send"(data(c'))]
          ["rcv"(data(d))])
          ["decrypt"(<data(n), PrivateKey(B), d>)]



Definitions occuring in Statement :  basic-seq-1-5: A ─→ B: pas[A;B;m;n;x;y;z] mk-pa: n(v) ses-public-key: PublicKey(A) ses-private-key: PrivateKey(A) sdata-pair: <d1, d2> atom-sdata: data(a) id-sdata: data(x) append: as bs cons: [a b] nil: [] pair: <a, b> token: "$token"
FDL editor aliases :  NSL-responder3

Latex:
NSL-responder3  ==
    B  {}\mrightarrow{}  A:  (["rcv"(data(c));
                        "decrypt"(<<data(m),  data(A)>,  PrivateKey(B),  c>);
                        "new"(n);
                        "encrypt"(<<data(m),  <data(n),  data(B)>>,  PublicKey(A),  c'>);
                        "send"(data(c'))]
                    @  ["rcv"(data(d))])
                    @  ["decrypt"(<data(n),  PrivateKey(B),  d>)]



Date html generated: 2015_07_23-PM-00_25_50
Last ObjectModification: 2012_08_30-PM-05_48_26

Home Index