---

{ ([a:Atom1]. ("new"(a)  ProtocolAction))
 ([d:SecurityData]. ("send"(d)  ProtocolAction))
 ([d:SecurityData]. ("rcv"(d)  ProtocolAction))
 ([tr:SecurityData  Key  Atom1]. ("encrypt"(tr)  ProtocolAction))
 ([tr:SecurityData  Key  Atom1]. ("decrypt"(tr)  ProtocolAction))
 ([tr:SecurityData  Id  Atom1]. ("sign"(tr)  ProtocolAction))
 ([tr:SecurityData  Id  Atom1]. ("verify"(tr)  ProtocolAction)) }

{ Proof }

---

Definitions occuring in Statement :  mk-pa: n(v),  protocol-action: ProtocolAction,  encryption-key: Key,  sdata: SecurityData,  Id: Id,  uall: [x:A]. B[x],  and: P  Q,  member: t  T,  product: x:A  B[x],  token: "$token",  atom: Atom$n
Definitions :  and: P  Q,  uall: [x:A]. B[x],  member: t  T,  protocol-action: ProtocolAction,  mk-pa: n(v),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  btrue: tt,  bfalse: ff
Lemmas :  ifthenelse_wf,  eq_atom_wf,  sdata_wf,  encryption-key_wf,  Id_wf,  top_wf

---

(\mforall{}[a:Atom1].  ("new"(a)  \mmember{}  ProtocolAction))
\mwedge{}  (\mforall{}[d:SecurityData].  ("send"(d)  \mmember{}  ProtocolAction))
\mwedge{}  (\mforall{}[d:SecurityData].  ("rcv"(d)  \mmember{}  ProtocolAction))
\mwedge{}  (\mforall{}[tr:SecurityData  \mtimes{}  Key  \mtimes{}  Atom1].  ("encrypt"(tr)  \mmember{}  ProtocolAction))
\mwedge{}  (\mforall{}[tr:SecurityData  \mtimes{}  Key  \mtimes{}  Atom1].  ("decrypt"(tr)  \mmember{}  ProtocolAction))
\mwedge{}  (\mforall{}[tr:SecurityData  \mtimes{}  Id  \mtimes{}  Atom1].  ("sign"(tr)  \mmember{}  ProtocolAction))
\mwedge{}  (\mforall{}[tr:SecurityData  \mtimes{}  Id  \mtimes{}  Atom1].  ("verify"(tr)  \mmember{}  ProtocolAction))


Date html generated: 2011_08_17-PM-07_40_03
Last ObjectModification: 2011_06_18-PM-01_33_10

Home Index