Step
*
2
of Lemma
ses-ordering-ordering'
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. ∀m:ℕ. ∀b:E.
((∀n:E(New). ∀e':E.
(((e' has New(n)) ∧ (e' ->>^m b))
⇒ (n ≤loc b ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
∧ (∀e1:E(Sign). ∀e':E.
(((e' has signature(e1)) ∧ (e' ->>^m b))
⇒ (∃e2:E(Sign)
((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))))))))
∧ (∀e1:E(Encrypt). ∀e':E.
(((e' has cipherText(e1)) ∧ (e' ->>^m b))
⇒ (∃e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))))
⊢ ∀b:E
((∀n:E(New). (b has* New(n)
⇒ (n ≤loc b ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
∧ (∀e1:E(Sign)
(b has* signature(e1)
⇒ (∃e2:E(Sign)
((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))))))))
∧ (∀e1:E(Encrypt)
(b has* cipherText(e1)
⇒ (∃e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))))
BY
{ ((D 0 THENA Auto)
THEN SplitAndConcl
THEN RepeatFor 2 ((D 0 THENA Auto))
THEN RepeatFor 2 (D (-1))
THEN RepUR ``rel_star`` (-1)
THEN D -1
THEN RenameVar `m' (-2)
THEN (InstHyp [⌈m⌉;⌈b⌉] 5⋅ THENA Auto)
THEN SplitAndHyps
THEN (UsingVars [`e\''] (BackThruSomeHyp) THEN Auto)⋅)⋅ }
Latex:
Latex:
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. \mforall{}m:\mBbbN{}. \mforall{}b:E.
((\mforall{}n:E(New). \mforall{}e':E.
(((e' has New(n)) \mwedge{} (e' rel\_exp(E; ->> m) b))
{}\mRightarrow{} (n \mleq{}loc b \mvee{} (\mexists{}snd:E(Send). ((n <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* New(n))))))
\mwedge{} (\mforall{}e1:E(Sign). \mforall{}e':E.
(((e' has signature(e1)) \mwedge{} (e' rel\_exp(E; ->> m) b))
{}\mRightarrow{} (\mexists{}e2:E(Sign)
((Sign(e2) = Sign(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* signature(e1))))))))
\mwedge{} (\mforall{}e1:E(Encrypt). \mforall{}e':E.
(((e' has cipherText(e1)) \mwedge{} (e' rel\_exp(E; ->> m) b))
{}\mRightarrow{} (\mexists{}e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* cipherText(e1)))))))))
\mvdash{} \mforall{}b:E
((\mforall{}n:E(New)
(b has* New(n)
{}\mRightarrow{} (n \mleq{}loc b \mvee{} (\mexists{}snd:E(Send). ((n <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* New(n))))))
\mwedge{} (\mforall{}e1:E(Sign)
(b has* signature(e1)
{}\mRightarrow{} (\mexists{}e2:E(Sign)
((Sign(e2) = Sign(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* signature(e1))))))))
\mwedge{} (\mforall{}e1:E(Encrypt)
(b has* cipherText(e1)
{}\mRightarrow{} (\mexists{}e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* cipherText(e1)))))))))
By
Latex:
((D 0 THENA Auto)
THEN SplitAndConcl
THEN RepeatFor 2 ((D 0 THENA Auto))
THEN RepeatFor 2 (D (-1))
THEN RepUR ``rel\_star`` (-1)
THEN D -1
THEN RenameVar `m' (-2)
THEN (InstHyp [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}] 5\mcdot{} THENA Auto)
THEN SplitAndHyps
THEN (UsingVars [`e\mbackslash{}''] (BackThruSomeHyp) THEN Auto)\mcdot{})\mcdot{}
Home
Index