---

UniqueSignatures(bss) ==
  A:Id
    (Honest(A)
     (Protocol1(bss) A)
     (es:EO+(Info). thr:Thread.
          ((thr is one of bss at A)  noncelike-signatures(s;es;thr))))

---

Definitions :  Id: Id,  ses-honest: Honest(A),  apply: f a,  ses-protocol1: Protocol1(bss),  event-ordering+: EO+(Info),  ses-info: Info,  all: x:A. B[x],  ses-thread: Thread,  implies: P  Q,  ses-protocol1-thread: (thr is one of bss at A),  noncelike-signatures: noncelike-signatures(s;es;thr)
FDL editor aliases :  unique-sig-protocol

---

UniqueSignatures(bss)  ==
    \mforall{}A:Id
        (Honest(A)
        {}\mRightarrow{}  (Protocol1(bss)  A)
        {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}thr:Thread.    ((thr  is  one  of  bss  at  A)  {}\mRightarrow{}  noncelike-signatures(s;es;thr))))


Date html generated: 2010_08_28-AM-03_15_08
Last ObjectModification: 2010_03_15-AM-11_30_16

Home Index