Nuprl Definition : ses-ordering'
ses-ordering'(s) ==
∀es:EO+(Info). ∀b:E.
((∀n:E(New). (b has* New(n) ⇒ (n ≤loc b ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
∧ (∀e1:E(Sign)
(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 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,
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:
ses-ordering'(s) ==
\mforall{}es:EO+(Info). \mforall{}b:E.
((\mforall{}n:E(New)
(b has* New(n)
{}\mRightarrow{} (n \mleq{}loc b \mvee{} (\mexists{}snd:E(Send). ((n <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* New(n))))))
\mwedge{} (\mforall{}e1:E(Sign)
(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)
(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_07
Last ObjectModification:
2012_08_30-PM-04_22_32
Home
Index