---

{ [s:SES]. [prtcl:Id  ']. [bs:Basic1]. [n:].
    (prtcl |= bs authenticates n messages   ') }

{ Proof }

---

Definitions occuring in Statement :  authentication: prtcl |= bs authenticates n messages ,  ses-basic-sequence1: Basic1,  security-event-structure: SES,  Id: Id,  nat: ,  uall: [x:A]. B[x],  prop: ,  member: t  T,  function: x:A  B[x]
Definitions :  uall: [x:A]. B[x],  prop: ,  member: t  T,  authentication: prtcl |= bs authenticates n messages ,  all: x:A. B[x],  implies: P  Q,  and: P  Q,  exists: x:A. B[x]
Lemmas :  event-ordering+_wf,  ses-info_wf,  Id_wf,  ses-honest_wf,  not_wf,  ses-thread_wf,  ses-thread-loc_wf,  is-basic-seq_wf,  matching-conversation_wf,  nat_wf,  ses-basic-sequence1_wf,  security-event-structure_wf

---

\mforall{}[s:SES].  \mforall{}[prtcl:Id  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[bs:Basic1].  \mforall{}[n:\mBbbN{}].    (prtcl  |=  bs  authenticates  n  messages    \mmember{}  \mBbbP{}')


Date html generated: 2011_08_17-PM-07_41_57
Last ObjectModification: 2011_06_18-PM-01_35_39

Home Index