---

PropertyD ==
  es:EO+(Info). e:E(Decrypt).
    e':E(Encrypt)
     ((e' < e)
      (plainText(e) = plainText(e'))
      (cipherText(e) = cipherText(e'))
      MatchingKeys(key(e);key(e')))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  all: x:A. B[x],  ses-decrypt: Decrypt,  exists: x:A. B[x],  es-E-interface: E(X),  ses-encrypt: Encrypt,  es-causl: (e < e'),  sdata: SecurityData,  ses-decrypted: plainText(e),  ses-encrypted: plainText(e),  and: P  Q,  equal: s = t,  atom: Atom$n,  ses-cipher: cipherText(e),  ses-crypt: cipherText(e),  ses-key-rel: MatchingKeys(k1;k2),  ses-decryption-key: key(e),  ses-encryption-key: key(e)
FDL editor aliases :  ses-D

---

PropertyD  ==
    \mforall{}es:EO+(Info).  \mforall{}e:E(Decrypt).
        \mexists{}e':E(Encrypt)
          ((e'  <  e)
          \mwedge{}  (plainText(e)  =  plainText(e'))
          \mwedge{}  (cipherText(e)  =  cipherText(e'))
          \mwedge{}  MatchingKeys(key(e);key(e')))


Date html generated: 2010_08_28-AM-02_34_09
Last ObjectModification: 2010_02_22-PM-05_30_41

Home Index