PropertyS ==
es:EO+(Info)
((A:Id. (Honest(A) 
(e:E(Sign). ((signer(e) = A) (loc(e) = A)))))
(A:Id
(Honest(A)
((e:E(Encrypt). ((key(e) = PrivateKey(A)) (loc(e) = A)))
(e:E(Decrypt). ((key(e) = PrivateKey(A)) (loc(e) = A)))))))
Definitions :
event-ordering+: EO+(Info),
ses-info: Info,
ses-sign: Sign,
ses-signer: signer(e),
ses-honest: Honest(A),
and: P Q,
ses-encrypt: Encrypt,
ses-encryption-key: key(e),
all: x:A. B[x],
es-E-interface: E(X),
ses-decrypt: Decrypt,
implies: P Q,
encryption-key: Key,
ses-decryption-key: key(e),
ses-private-key: PrivateKey(A),
equal: s = t,
Id: Id,
es-loc: loc(e)
FDL editor aliases :
ses-S
PropertyS ==
\mforall{}es:EO+(Info)
((\mforall{}A:Id. (Honest(A) {}\mRightarrow{} (\mforall{}e:E(Sign). ((signer(e) = A) {}\mRightarrow{} (loc(e) = A)))))
\mwedge{} (\mforall{}A:Id
(Honest(A)
{}\mRightarrow{} ((\mforall{}e:E(Encrypt). ((key(e) = PrivateKey(A)) {}\mRightarrow{} (loc(e) = A)))
\mwedge{} (\mforall{}e:E(Decrypt). ((key(e) = PrivateKey(A)) {}\mRightarrow{} (loc(e) = A)))))))
Date html generated:
2010_08_28-AM-02_34_30
Last ObjectModification:
2010_02_22-PM-05_33_25
Home
Index