Nuprl Definition : ses-K
PropertyK ==
Sym(Key;k1,k2.MatchingKeys(k1;k2))
∧ (∀A:Id. ∀k:Key. (MatchingKeys(PrivateKey(A);k) ⇐⇒ k = PublicKey(A) ∈ Key))
∧ (∀A:Id. ∀k:Key. (MatchingKeys(PublicKey(A);k) ⇐⇒ k = PrivateKey(A) ∈ Key))
∧ (∀A,B:Id. (Private(A) = Private(B) ∈ Atom1 ⇐⇒ A = B ∈ Id))
∧ (∀a:Atom1. ∀k:Key. (MatchingKeys(symmetric-key(a);k) ⇐⇒ k = symmetric-key(a) ∈ Key))
Definitions occuring in Statement :
ses-public-key: PublicKey(A),
ses-private-key: PrivateKey(A),
ses-private: Private(A),
ses-key-rel: MatchingKeys(k1;k2),
symmetric-key: symmetric-key(a),
encryption-key: Key,
Id: Id,
sym: Sym(T;x,y.E[x; y]),
atom: Atom$n,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
ses-K
Latex:
PropertyK ==
Sym(Key;k1,k2.MatchingKeys(k1;k2))
\mwedge{} (\mforall{}A:Id. \mforall{}k:Key. (MatchingKeys(PrivateKey(A);k) \mLeftarrow{}{}\mRightarrow{} k = PublicKey(A)))
\mwedge{} (\mforall{}A:Id. \mforall{}k:Key. (MatchingKeys(PublicKey(A);k) \mLeftarrow{}{}\mRightarrow{} k = PrivateKey(A)))
\mwedge{} (\mforall{}A,B:Id. (Private(A) = Private(B) \mLeftarrow{}{}\mRightarrow{} A = B))
\mwedge{} (\mforall{}a:Atom1. \mforall{}k:Key. (MatchingKeys(symmetric-key(a);k) \mLeftarrow{}{}\mRightarrow{} k = symmetric-key(a)))
Date html generated:
2016_05_17-PM-00_25_31
Last ObjectModification:
2012_08_30-PM-04_24_45
Theory : event-logic-applications
Home
Index