Step
*
of Lemma
ses-sign-is-protocol-action
∀[s:SES]
∀[pa:ProtocolAction]. ∀[es:EO+(Info)]. ∀[e:E].
({((fst(pa)) = "sign" ∈ Atom) ∧ ((snd(pa)) = Sign(e) ∈ (SecurityData × Id × Atom1))}) supposing
((↑e ∈b Sign) and
pa(e))
supposing ActionsDisjoint
BY
{ ((UnivCD THENA Auto)
THEN MoveToConcl (-2)
THEN DVar `pa'
THEN RepUR ``ses-is-protocol-action`` 0
THEN MoveToConcl (-4)
THEN (With ⌈es⌉ (D 2)⋅ THENA Auto)
THEN (D -1 THEN (InstHyp [⌈e⌉] (-1)⋅ THENA Auto) THEN SplitAndHyps)
THEN Repeat ((WeakAutoSplit THENL [Auto; Id]))
THEN Auto) }
Latex:
Latex:
\mforall{}[s:SES]
\mforall{}[pa:ProtocolAction]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E].
(\{((fst(pa)) = "sign") \mwedge{} ((snd(pa)) = Sign(e))\}) supposing ((\muparrow{}e \mmember{}\msubb{} Sign) and pa(e))
supposing ActionsDisjoint
By
Latex:
((UnivCD THENA Auto)
THEN MoveToConcl (-2)
THEN DVar `pa'
THEN RepUR ``ses-is-protocol-action`` 0
THEN MoveToConcl (-4)
THEN (With \mkleeneopen{}es\mkleeneclose{} (D 2)\mcdot{} THENA Auto)
THEN (D -1 THEN (InstHyp [\mkleeneopen{}e\mkleeneclose{}] (-1)\mcdot{} THENA Auto) THEN SplitAndHyps)
THEN Repeat ((WeakAutoSplit THENL [Auto; Id]))
THEN Auto)
Home
Index