Nuprl Definition : ses-nonce-disjoint

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

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

Latex:
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: 2016_05_17-PM-00_26_11 Last ObjectModification: 2012_08_30-PM-04_25_08 Theory : event-logic-applications Home Index