Nuprl Definition : ses-D-public
ses-D-public(s) ==
∀es:EO+(Info). ∀e:E(Decrypt). ∀A:Id. ∀d:SecurityData. ∀c:Atom1.
((Decrypt(e) = <d, PublicKey(A), c> ∈ (SecurityData × Key × Atom1))
⇒ (∃e':E(Encrypt). ((e' < e) ∧ (Encrypt(e') = <d, PrivateKey(A), c> ∈ (SecurityData × Key × Atom1)))))
Definitions occuring in Statement :
ses-public-key: PublicKey(A),
ses-private-key: PrivateKey(A),
ses-decrypt: Decrypt,
ses-encrypt: Encrypt,
ses-info: Info,
encryption-key: Key,
sdata: SecurityData,
es-E-interface: E(X),
eclass-val: X(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
Id: Id,
atom: Atom$n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
pair: <a, b>,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
ses-D-public
Latex:
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:
2016_05_17-PM-00_26_36
Last ObjectModification:
2012_08_30-PM-04_25_29
Theory : event-logic-applications
Home
Index