Nuprl Definition : ses-ordering
PropertyO ==
∀es:EO+(Info)
((∀n:E(New). ∀e:E. ((e has New(n)) ⇒ (n ≤loc e ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n))))))
∧ (∀e1:E(Sign). ∀b:E.
((b has signature(e1))
⇒ (∃e2:E(Sign)
((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))))))))
∧ (∀e1:E(Encrypt). ∀b:E.
((b has cipherText(e1))
⇒ (∃e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))))
Definitions occuring in Statement :
event-has*: e has* a,
event-has: (e has a),
ses-crypt: cipherText(e),
ses-encrypt: Encrypt,
ses-sig: signature(e),
ses-sign: Sign,
ses-send: Send,
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-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-causl: (e < e'),
es-E: E,
Id: Id,
atom: Atom$n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
ses-ordering
Latex:
PropertyO ==
\mforall{}es:EO+(Info)
((\mforall{}n:E(New). \mforall{}e:E.
((e has New(n))
{}\mRightarrow{} (n \mleq{}loc e \mvee{} (\mexists{}snd:E(Send). ((n <loc snd) \mwedge{} (snd < e) \mwedge{} snd has* New(n))))))
\mwedge{} (\mforall{}e1:E(Sign). \mforall{}b:E.
((b has signature(e1))
{}\mRightarrow{} (\mexists{}e2:E(Sign)
((Sign(e2) = Sign(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* signature(e1))))))))
\mwedge{} (\mforall{}e1:E(Encrypt). \mforall{}b:E.
((b has cipherText(e1))
{}\mRightarrow{} (\mexists{}e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* cipherText(e1)))))))))
Date html generated:
2015_07_23-PM-00_06_02
Last ObjectModification:
2012_08_30-PM-04_22_23
Home
Index