---

ses-D-public(s) ==
  es:EO+(Info). e:E(Decrypt). A:Id. d:SecurityData. c:Atom1.
    ((Decrypt(e) = <d, PublicKey(A), c>)
     (e':E(Encrypt). ((e' < e)  (Encrypt(e') = <d, PrivateKey(A), c>))))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  Id: Id,  all: x:A. B[x],  implies: P  Q,  ses-decrypt: Decrypt,  ses-public-key: PublicKey(A),  exists: x:A. B[x],  es-E-interface: E(X),  and: P  Q,  es-causl: (e < e'),  equal: s = t,  sdata: SecurityData,  product: x:A  B[x],  encryption-key: Key,  atom: Atom$n,  eclass-val: X(e),  ses-encrypt: Encrypt,  pair: <a, b>,  ses-private-key: PrivateKey(A)
FDL editor aliases :  ses-D-public

---

ses-D-public(s)  ==
    \mforall{}es:EO+(Info).  \mforall{}e:E(Decrypt).  \mforall{}A:Id.  \mforall{}d:SecurityData.  \mforall{}c:Atom1.
        ((Decrypt(e)  =  <d,  PublicKey(A),  c>)
        {}\mRightarrow{}  (\mexists{}e':E(Encrypt).  ((e'  <  e)  \mwedge{}  (Encrypt(e')  =  <d,  PrivateKey(A),  c>))))


Date html generated: 2010_08_28-AM-02_35_48
Last ObjectModification: 2010_02_22-PM-05_49_18

Home Index