---

->> ==  e',e.((e'  Encrypt)  (e has cipherText(e')))

---

Definitions :  lambda: x.A[x],  and: P  Q,  assert: b,  in-eclass: e  X,  ses-encrypt: Encrypt,  event-has: (e has a),  ses-crypt: cipherText(e)
FDL editor aliases :  ses-info-flow

---

->>  ==    \mlambda{}e',e.((\muparrow{}e'  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (e  has  cipherText(e')))


Date html generated: 2010_08_28-AM-02_07_51
Last ObjectModification: 2010_02_22-PM-02_08_04

Home Index