Nuprl Definition : ses-D

PropertyD ==
  ∀es:EO+(Info). ∀e:E(Decrypt).
    ∃e':E(Encrypt)
     ((e' < e)
     ∧ (plainText(e) = plainText(e') ∈ SecurityData)
     ∧ (cipherText(e) = cipherText(e') ∈ Atom1)
     ∧ MatchingKeys(key(e);key(e')))

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

Latex:
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: 2016_05_17-PM-00_25_05 Last ObjectModification: 2012_08_30-PM-04_24_29 Theory : event-logic-applications Home Index