---

NoncesCiphersAndKeysDisjoint ==
  es:EO+(Info)
    ((n:E(New). e:E(Sign).  ((New(n) = signature(e))))
     (n:E(New). e:E(Encrypt).  ((New(n) = cipherText(e))))
     (n:E(New). A:Id.  ((New(n) = Private(A))))
     (A:Id. e:E(Encrypt).  ((cipherText(e) = Private(A))))
     (A:Id. e:E(Sign).  ((signature(e) = Private(A))))
     (e1:E(Sign). e2:E(Encrypt).  ((signature(e1) = cipherText(e2)))))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  eclass-val: X(e),  ses-new: New,  and: P  Q,  Id: Id,  ses-private: Private(A),  ses-sign: Sign,  all: x:A. B[x],  es-E-interface: E(X),  ses-encrypt: Encrypt,  not: A,  equal: s = t,  atom: Atom$n,  ses-sig: signature(e),  ses-crypt: cipherText(e)
FDL editor aliases :  ses-nonce-disjoint

---

NoncesCiphersAndKeysDisjoint  ==
    \mforall{}es:EO+(Info)
        ((\mforall{}n:E(New).  \mforall{}e:E(Sign).    (\mneg{}(New(n)  =  signature(e))))
        \mwedge{}  (\mforall{}n:E(New).  \mforall{}e:E(Encrypt).    (\mneg{}(New(n)  =  cipherText(e))))
        \mwedge{}  (\mforall{}n:E(New).  \mforall{}A:Id.    (\mneg{}(New(n)  =  Private(A))))
        \mwedge{}  (\mforall{}A:Id.  \mforall{}e:E(Encrypt).    (\mneg{}(cipherText(e)  =  Private(A))))
        \mwedge{}  (\mforall{}A:Id.  \mforall{}e:E(Sign).    (\mneg{}(signature(e)  =  Private(A))))
        \mwedge{}  (\mforall{}e1:E(Sign).  \mforall{}e2:E(Encrypt).    (\mneg{}(signature(e1)  =  cipherText(e2)))))


Date html generated: 2010_08_28-AM-02_35_17
Last ObjectModification: 2010_02_22-PM-05_44_40

Home Index