---

FreshSignatures(bss) ==
  f:SecurityData  (?Atom1)
   es:EO+(Info). thr:Thread. A:Id.
     ((thr is one of bss at A)  ses-fresh-thread(s;es;f;A;thr))

---

Definitions :  exists: x:A. B[x],  function: x:A  B[x],  sdata: SecurityData,  union: left + right,  atom: Atom$n,  unit: Unit,  event-ordering+: EO+(Info),  ses-info: Info,  ses-thread: Thread,  all: x:A. B[x],  Id: Id,  implies: P  Q,  ses-protocol1-thread: (thr is one of bss at A),  ses-fresh-thread: ses-fresh-thread(s;es;f;A;thr)
FDL editor aliases :  fresh-sig-protocol1

---

FreshSignatures(bss)  ==
    \mexists{}f:SecurityData  {}\mrightarrow{}  (?Atom1)
      \mforall{}es:EO+(Info).  \mforall{}thr:Thread.  \mforall{}A:Id.    ((thr  is  one  of  bss  at  A)  {}\mRightarrow{}  ses-fresh-thread(s;es;f;A;thr))


Date html generated: 2010_08_28-AM-03_15_01
Last ObjectModification: 2010_03_16-PM-03_43_38

Home Index