cabal is a cabal for atms ==
(
a
atms.(
icabal. e:E
((loc(e) = i)
(((
e 
New) (a = New(e)))
((e Encrypt)
(a = cipherText(e))
(batms. (
(b = a)) (e has b))))))
(e:E(Send). ((loc(e) cabal) 
((e has a))))
(e:E(Encrypt)
((loc(e) cabal)
(e has a)
((Acabal. key(e) = PublicKey(A))
(katms. key(e) = symmetric-key(k))
(cipherText(e) atms)))))
Definitions :
l_all: (xL.P[x]),
exists: x:A. B[x],
es-E: E,
eclass-val: X(e),
ses-new: New,
assert: b,
in-eclass: e X,
and: P Q,
ses-send: Send,
not: A,
all: x:A. B[x],
es-E-interface: E(X),
ses-encrypt: Encrypt,
es-loc: loc(e),
implies: P Q,
event-has: (e has a),
Id: Id,
ses-public-key: PublicKey(A),
or: P Q,
l_exists: (xL. P[x]),
equal: s = t,
encryption-key: Key,
ses-encryption-key: key(e),
symmetric-key: symmetric-key(a),
l_member: (x l),
ses-crypt: cipherText(e),
atom: Atom$n
FDL editor aliases :
ses-cabal
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:
2010_08_28-AM-02_08_45
Last ObjectModification:
2010_03_10-PM-11_01_42
Home
Index