---

Step * of Lemma mk-pa_wf

(∀[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))
BY
{ (Auto
   THEN Unfolds ``mk-pa protocol-action`` 0
   THEN Auto
   THEN SymbolicCompute [`sdata`;`encryption-key`] [] [] 0
   THEN Auto) }

---

Latex:

---

Latex:
(\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))


By

---

Latex:
(Auto
  THEN  Unfolds  ``mk-pa  protocol-action``  0
  THEN  Auto
  THEN  SymbolicCompute  [`sdata`;`encryption-key`]  []  []  0
  THEN  Auto)

---

Home Index