Step
*
1
2
1
1
1
3
1
of Lemma
ses-ordering-ordering'
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕ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)))))))))@i
7. b : E@i
8. ∀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)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(z)))
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
23. e3 ≤loc e2 ∨ (∃snd:E(Send). ((e3 <loc snd) ∧ (snd < e2) ∧ snd has* signature(e1)))
24. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
25. ¬e3 ≤loc b
⊢ ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))
BY
{ SplitOrHyps }
1
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕ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)))))))))@i
7. b : E@i
8. ∀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)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. e2 ≤loc b
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
23. e3 ≤loc e2
24. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
25. ¬e3 ≤loc b
⊢ ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))
2
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕ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)))))))))@i
7. b : E@i
8. ∀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)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. ∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(z))
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
23. e3 ≤loc e2
24. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
25. ¬e3 ≤loc b
⊢ ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))
3
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕ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)))))))))@i
7. b : E@i
8. ∀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)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. e2 ≤loc b
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
23. ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < e2) ∧ snd has* signature(e1))
24. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
25. ¬e3 ≤loc b
⊢ ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))
4
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕ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)))))))))@i
7. b : E@i
8. ∀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)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. ∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(z))
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
23. ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < e2) ∧ snd has* signature(e1))
24. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
25. ¬e3 ≤loc b
⊢ ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))
Latex:
Latex:
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : \mBbbN{}
6. \mforall{}m:\mBbbN{}m. \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)))))))))@i
7. b : E@i
8. \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)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' rel\_exp(E; ->> m - 1) z
15. \muparrow{}z \mmember{}\msubb{} Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z)
19. e2 \mleq{}loc b \mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* cipherText(z)))
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1)
23. e3 \mleq{}loc e2 \mvee{} (\mexists{}snd:E(Send). ((e3 <loc snd) \mwedge{} (snd < e2) \mwedge{} snd has* signature(e1)))
24. Sign(e3) = Sign(e1)
25. \mneg{}e3 \mleq{}loc b
\mvdash{} \mexists{}snd:E(Send). ((e3 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* signature(e1))
By
Latex:
SplitOrHyps
Home
Index