---

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

---

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

---

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: 2010_08_28-AM-03_13_43
Last ObjectModification: 2010_02_23-AM-10_46_26

Home Index