---

PropertyK ==
  Sym(Key;k1,k2.MatchingKeys(k1;k2))
   (A:Id. k:Key.  (MatchingKeys(PrivateKey(A);k)  k = PublicKey(A)))
   (A:Id. k:Key.  (MatchingKeys(PublicKey(A);k)  k = PrivateKey(A)))
   (A,B:Id.  (Private(A) = Private(B)  A = B))
   (a:Atom1. k:Key.
       (MatchingKeys(symmetric-key(a);k)  k = symmetric-key(a)))

---

Definitions :  sym: Sym(T;x,y.E[x; y]),  ses-public-key: PublicKey(A),  ses-private-key: PrivateKey(A),  and: P  Q,  ses-private: Private(A),  Id: Id,  atom: Atom$n,  all: x:A. B[x],  iff: P  Q,  ses-key-rel: MatchingKeys(k1;k2),  equal: s = t,  encryption-key: Key,  symmetric-key: symmetric-key(a)
FDL editor aliases :  ses-K

---

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: 2010_08_28-AM-02_34_39
Last ObjectModification: 2010_03_11-PM-04_15_41

Home Index