Step
*
1
1
2
1
1
1
2
of Lemma
ses-legal-thread-has*-nonce
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a ∈ thr@i
11. a has* New(n)@i
12. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* New(n) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
13. ¬(a = n ∈ E)
14. e : E@i
15. ∀e1:E
((e1 < e)
⇒ Action(e1)
⇒ e1 ∈ thr
⇒ e1 ≤loc a
⇒ (∀m:ℕ. ∀e':E.
((e' ->>^m e1)
⇒ (e' has New(n))
⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e1 = n ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. m : ℤ@i
20. \\%24 : 0 < m@i
21. ∀e':E
((e' ->>^m - 1 e)
⇒ (e' has New(n))
⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)))@i
22. e' : E@i
23. z : E
24. 0 < m
25. e' ->>^m - 1 z
26. ↑z ∈b Encrypt
27. (e has cipherText(z))
28. (e' has New(n))@i
29. z has* New(n)
30. e1 : Act
31. (e1 <loc e)
32. (e1 has cipherText(z))
33. e1 ∈ thr
34. e1 has* New(n)
⊢ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)
BY
{ (RepeatFor 2 (D -1)
THEN RepUR ``rel_star`` -1
THEN ExRepD
THEN OnMaybeHyp 8 (\h. (InstHyp [⌈e1⌉;⌈n1⌉;⌈e2⌉] h⋅ THENA (Auto THEN Try ((BackThruSomeHyp THEN Auto)))))) }
1
.....antecedent.....
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a ∈ thr@i
11. a has* New(n)@i
12. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* New(n) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
13. ¬(a = n ∈ E)
14. e : E@i
15. ∀e1:E
((e1 < e)
⇒ Action(e1)
⇒ e1 ∈ thr
⇒ e1 ≤loc a
⇒ (∀m:ℕ. ∀e':E.
((e' ->>^m e1)
⇒ (e' has New(n))
⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e1 = n ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. m : ℤ@i
20. \\%24 : 0 < m@i
21. ∀e':E
((e' ->>^m - 1 e)
⇒ (e' has New(n))
⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)))@i
22. e' : E@i
23. z : E
24. 0 < m
25. e' ->>^m - 1 z
26. ↑z ∈b Encrypt
27. (e has cipherText(z))
28. (e' has New(n))@i
29. z has* New(n)
30. e1 : Act
31. (e1 <loc e)
32. (e1 has cipherText(z))
33. e1 ∈ thr
34. e2 : E
35. (e2 has New(n))
36. n1 : ℕ
37. e2 ->>^n1 e1
⊢ Action(e1)
2
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a ∈ thr@i
11. a has* New(n)@i
12. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* New(n) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
13. ¬(a = n ∈ E)
14. e : E@i
15. ∀e1:E
((e1 < e)
⇒ Action(e1)
⇒ e1 ∈ thr
⇒ e1 ≤loc a
⇒ (∀m:ℕ. ∀e':E.
((e' ->>^m e1)
⇒ (e' has New(n))
⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e1 = n ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. m : ℤ@i
20. \\%24 : 0 < m@i
21. ∀e':E
((e' ->>^m - 1 e)
⇒ (e' has New(n))
⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)))@i
22. e' : E@i
23. z : E
24. 0 < m
25. e' ->>^m - 1 z
26. ↑z ∈b Encrypt
27. (e has cipherText(z))
28. (e' has New(n))@i
29. z has* New(n)
30. e1 : Act
31. (e1 <loc e)
32. (e1 has cipherText(z))
33. e1 ∈ thr
34. e2 : E
35. (e2 has New(n))
36. n1 : ℕ
37. e2 ->>^n1 e1
38. (∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e1 = n ∈ E)
⊢ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)
Latex:
Latex:
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a \mmember{} thr@i
11. a has* New(n)@i
12. \mforall{}e':E. ((e' < a) {}\mRightarrow{} Action(e') {}\mRightarrow{} e' has* New(n) {}\mRightarrow{} ((loc(e') = A) \mwedge{} (\mneg{}\muparrow{}e' \mmember{}\msubb{} Send)))
13. \mneg{}(a = n)
14. e : E@i
15. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} Action(e1)
{}\mRightarrow{} e1 \mmember{} thr
{}\mRightarrow{} e1 \mleq{}loc a
{}\mRightarrow{} (\mforall{}m:\mBbbN{}. \mforall{}e':E.
((e' rel\_exp(E; ->> m) e1)
{}\mRightarrow{} (e' has New(n))
{}\mRightarrow{} ((\mexists{}e':E. ((e' <loc e1) \mwedge{} Action(e') \mwedge{} e' has* New(n) \mwedge{} e' \mmember{} thr)) \mvee{} (e1 = n)))))
16. Action(e)@i
17. e \mmember{} thr@i
18. e \mleq{}loc a @i
19. m : \mBbbZ{}@i
20. \mbackslash{}\mbackslash{}\%24 : 0 < m@i
21. \mforall{}e':E
((e' rel\_exp(E; ->> m - 1) e)
{}\mRightarrow{} (e' has New(n))
{}\mRightarrow{} ((\mexists{}e':E. ((e' <loc e) \mwedge{} Action(e') \mwedge{} e' has* New(n) \mwedge{} e' \mmember{} thr)) \mvee{} (e = n)))@i
22. e' : E@i
23. z : E
24. 0 < m
25. e' rel\_exp(E; ->> m - 1) z
26. \muparrow{}z \mmember{}\msubb{} Encrypt
27. (e has cipherText(z))
28. (e' has New(n))@i
29. z has* New(n)
30. e1 : Act
31. (e1 <loc e)
32. (e1 has cipherText(z))
33. e1 \mmember{} thr
34. e1 has* New(n)
\mvdash{} (\mexists{}e':E. ((e' <loc e) \mwedge{} Action(e') \mwedge{} e' has* New(n) \mwedge{} e' \mmember{} thr)) \mvee{} (e = n)
By
Latex:
(RepeatFor 2 (D -1)
THEN RepUR ``rel\_star`` -1
THEN ExRepD
THEN OnMaybeHyp 8 (\mbackslash{}h. (InstHyp [\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}] h\mcdot{}
THENA (Auto THEN Try ((BackThruSomeHyp THEN Auto)))
)))
Home
Index