Nuprl Definition : unique-sig-protocol

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 occuring in Statement : ses-protocol1: Protocol1(bss), ses-protocol1-thread: (thr is one of bss at A), noncelike-signatures: noncelike-signatures(s;es;thr), ses-thread: Thread, ses-honest: Honest(A), ses-info: Info, event-ordering+: EO+(Info), Id: Id, all: ∀x:A. B[x], implies: P ⇒ Q, apply: f a
FDL editor aliases : unique-sig-protocol

Latex:
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: 2015_07_23-PM-00_17_28 Last ObjectModification: 2012_08_30-PM-04_34_00 Home Index