Nuprl Definition : authentication

prtcl |= bs authenticates n messages  ==
  ∀es:EO+(Info). ∀A,B:Id.
    ((Honest(A) ∧ Honest(B) ∧ (¬(A = B ∈ Id)) ∧ (prtcl A) ∧ (prtcl B))
    ⇒ (∀thr1:Thread
          (loc(thr1)= A ⇒ thr1[A;B] |= bs ⇒ (∃thr2:Thread. (MatchingConversation(n;thr1;thr2) ∧ loc(thr2)= B)))))

Definitions occuring in Statement : is-basic-seq: thr[A;B] |= bs, ses-thread-loc: loc(thr)= A, ses-thread: Thread, matching-conversation: MatchingConversation(n;thr1;thr2), ses-honest: Honest(A), ses-info: Info, event-ordering+: EO+(Info), Id: Id, all: ∀x:A. B[x], exists: ∃x:A. B[x], not: ¬A, implies: P ⇒ Q, and: P ∧ Q, apply: f a, equal: s = t ∈ T
FDL editor aliases : authentication

Latex:
prtcl |= bs authenticates n messages == \mforall{}es:EO+(Info). \mforall{}A,B:Id. ((Honest(A) \mwedge{} Honest(B) \mwedge{} (\mneg{}(A = B)) \mwedge{} (prtcl A) \mwedge{} (prtcl B)) {}\mRightarrow{} (\mforall{}thr1:Thread (loc(thr1)= A {}\mRightarrow{} thr1[A;B] |= bs {}\mRightarrow{} (\mexists{}thr2:Thread. (MatchingConversation(n;thr1;thr2) \mwedge{} loc(thr2)= B))))) Date html generated: 2016_05_17-PM-00_41_06 Last ObjectModification: 2012_08_30-PM-04_32_31 Theory : event-logic-applications Home Index