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