Nuprl Definition : ses-S

PropertyS ==
  ∀es:EO+(Info)
    ((∀A:Id. (Honest(A) ⇒ (∀e:E(Sign). ((signer(e) = A ∈ Id) ⇒ (loc(e) = A ∈ Id)))))
    ∧ (∀A:Id
         (Honest(A)
         ⇒ ((∀e:E(Encrypt). ((key(e) = PrivateKey(A) ∈ Key) ⇒ (loc(e) = A ∈ Id)))
            ∧ (∀e:E(Decrypt). ((key(e) = PrivateKey(A) ∈ Key) ⇒ (loc(e) = A ∈ Id)))))))

Definitions occuring in Statement : ses-private-key: PrivateKey(A), ses-honest: Honest(A), ses-decryption-key: key(e), ses-decrypt: Decrypt, ses-encryption-key: key(e), ses-encrypt: Encrypt, ses-signer: signer(e), ses-sign: Sign, ses-info: Info, encryption-key: Key, es-E-interface: E(X), event-ordering+: EO+(Info), es-loc: loc(e), Id: Id, all: ∀x:A. B[x], implies: P ⇒ Q, and: P ∧ Q, equal: s = t ∈ T
FDL editor aliases : ses-S

Latex:
PropertyS == \mforall{}es:EO+(Info) ((\mforall{}A:Id. (Honest(A) {}\mRightarrow{} (\mforall{}e:E(Sign). ((signer(e) = A) {}\mRightarrow{} (loc(e) = A))))) \mwedge{} (\mforall{}A:Id (Honest(A) {}\mRightarrow{} ((\mforall{}e:E(Encrypt). ((key(e) = PrivateKey(A)) {}\mRightarrow{} (loc(e) = A))) \mwedge{} (\mforall{}e:E(Decrypt). ((key(e) = PrivateKey(A)) {}\mRightarrow{} (loc(e) = A))))))) Date html generated: 2016_05_17-PM-00_25_18 Last ObjectModification: 2012_08_30-PM-04_24_37 Theory : event-logic-applications Home Index