Nuprl Definition : ses-cabal
cabal is a cabal for atms ==
(∀a∈atms.(∃i∈cabal. ∃e:E
((loc(e) = i ∈ Id)
∧ (((↑e ∈b New) ∧ (a = New(e) ∈ Atom1))
∨ ((↑e ∈b Encrypt)
∧ (a = cipherText(e) ∈ Atom1)
∧ (∃b∈atms. (¬(b = a ∈ Atom1)) ∧ (e has b))))))
∧ (∀e:E(Send). ((loc(e) ∈ cabal) ⇒ (¬(e has a))))
∧ (∀e:E(Encrypt)
((loc(e) ∈ cabal)
⇒ (e has a)
⇒ ((∃A∈cabal. key(e) = PublicKey(A) ∈ Key)
∨ (∃k∈atms. key(e) = symmetric-key(k) ∈ Key)
∨ (cipherText(e) ∈ atms)))))
Definitions occuring in Statement :
event-has: (e has a),
ses-public-key: PublicKey(A),
ses-crypt: cipherText(e),
ses-encryption-key: key(e),
ses-encrypt: Encrypt,
ses-send: Send,
ses-new: New,
symmetric-key: symmetric-key(a),
encryption-key: Key,
es-E-interface: E(X),
eclass-val: X(e),
in-eclass: e ∈b X,
es-loc: loc(e),
es-E: E,
Id: Id,
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
atom: Atom$n,
assert: ↑b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
ses-cabal
Latex:
cabal is a cabal for atms ==
(\mforall{}a\mmember{}atms.(\mexists{}i\mmember{}cabal. \mexists{}e:E
((loc(e) = i)
\mwedge{} (((\muparrow{}e \mmember{}\msubb{} New) \mwedge{} (a = New(e)))
\mvee{} ((\muparrow{}e \mmember{}\msubb{} Encrypt)
\mwedge{} (a = cipherText(e))
\mwedge{} (\mexists{}b\mmember{}atms. (\mneg{}(b = a)) \mwedge{} (e has b))))))
\mwedge{} (\mforall{}e:E(Send). ((loc(e) \mmember{} cabal) {}\mRightarrow{} (\mneg{}(e has a))))
\mwedge{} (\mforall{}e:E(Encrypt)
((loc(e) \mmember{} cabal)
{}\mRightarrow{} (e has a)
{}\mRightarrow{} ((\mexists{}A\mmember{}cabal. key(e) = PublicKey(A))
\mvee{} (\mexists{}k\mmember{}atms. key(e) = symmetric-key(k))
\mvee{} (cipherText(e) \mmember{} atms)))))
Date html generated:
2016_05_17-AM-11_48_49
Last ObjectModification:
2013_10_01-PM-04_46_47
Theory : event-logic-applications
Home
Index