Nuprl Definition : ses-flow-axiom
PropertyF ==
∀es:EO+(Info)
((∀n:E(New). ∀e:E. ((e has New(n)) ⇒ ses-flow(s;es;New(n);n;e)))
∧ (∀e1:E(Sign). ∀b:E.
((b has signature(e1))
⇒ (∃e2:E(Sign). ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(s;es;signature(e2);e2;b)))))
∧ (∀e1:E(Encrypt). ∀b:E.
((b has cipherText(e1))
⇒ (∃e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1)) ∧ ses-flow(s;es;cipherText(e2);e2;b))))))
Definitions occuring in Statement :
ses-flow: ses-flow(s;es;a;e1;e2),
event-has: (e has a),
ses-crypt: cipherText(e),
ses-encrypt: Encrypt,
ses-sig: signature(e),
ses-sign: Sign,
ses-new: New,
ses-info: Info,
encryption-key: Key,
sdata: SecurityData,
es-E-interface: E(X),
eclass-val: X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
atom: Atom$n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
ses-flow-axiom
Latex:
PropertyF ==
\mforall{}es:EO+(Info)
((\mforall{}n:E(New). \mforall{}e:E. ((e has New(n)) {}\mRightarrow{} ses-flow(s;es;New(n);n;e)))
\mwedge{} (\mforall{}e1:E(Sign). \mforall{}b:E.
((b has signature(e1))
{}\mRightarrow{} (\mexists{}e2:E(Sign). ((Sign(e2) = Sign(e1)) \mwedge{} ses-flow(s;es;signature(e2);e2;b)))))
\mwedge{} (\mforall{}e1:E(Encrypt). \mforall{}b:E.
((b has cipherText(e1))
{}\mRightarrow{} (\mexists{}e2:E(Encrypt). ((Encrypt(e2) = Encrypt(e1)) \mwedge{} ses-flow(s;es;cipherText(e2);e2;b))))))
Date html generated:
2015_07_23-PM-00_06_13
Last ObjectModification:
2012_08_30-PM-04_22_40
Home
Index