Step
*
1
1
2
1
1
1
1
1
of Lemma
fresh-sig-protocol1_property
1. s : SES
2. ActionsDisjoint
3. PropertyO
4. PropertyS
5. bss : Basic1 List
6. f : SecurityData ⟶ (Atom1?)
7. A : Id@i
8. Honest(A)@i
9. ∀es:EO+(Info)
(Honest(A)
⇒ (∀e:Act
((loc(e) = A ∈ Id)
⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
∧ (∀thr1,thr2:Thread.
(e ∈ thr1
⇒ (thr1 is one of bss at A)
⇒ e ∈ thr2
⇒ (thr2 is one of bss at A)
⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))@i'
10. es : EO+(Info)@i'
11. E(Sign) ⊆r Act
12. ∀thr:Thread. ∀A:Id.
((thr is one of bss at A)
⇒ (∀i:ℕ||thr||
((↑thr[i] ∈b Sign)
⇒ ((signer(thr[i]) = A ∈ Id)
∧ (∃j:ℕi
((↑thr[j] ∈b New)
∧ (↑isl(f signed(thr[i])))
∧ (outl(f signed(thr[i])) = New(thr[j]) ∈ Atom1)
∧ (∀k:{j + 1..i-}
((↑thr[k] ∈b Sign)
⇒ (↑isl(f signed(thr[k])))
⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1))))))))))
13. e2 : E(Sign)@i
14. loc(e2) = A ∈ Id
15. thr2 : Thread
16. i : ℕ||thr2||
17. e2 = thr2[i] ∈ E
18. (thr2 is one of bss at A)
19. loc(thr2)= A
20. e1 : E(Sign)
21. Sign(e1) = Sign(e2) ∈ (SecurityData × Id × Atom1)
22. signer(e2) = A ∈ Id
23. signer(e1) = A ∈ Id
24. thr : Thread
25. i1 : ℕ||thr||
26. e1 = thr[i1] ∈ E
27. (thr is one of bss at A)
28. loc(thr)= A
29. ∀thr1,thr2:Thread.
(e1 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e1 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
30. signer(thr2[i]) = A ∈ Id
31. j1 : ℕi
32. ↑thr2[j1] ∈b New
33. ↑isl(f signed(thr2[i]))
34. outl(f signed(thr2[i])) = New(thr2[j1]) ∈ Atom1
35. ∀k:{j1 + 1..i-}
((↑thr2[k] ∈b Sign) ⇒ (↑isl(f signed(thr2[k]))) ⇒ (¬(outl(f signed(thr2[k])) = New(thr2[j1]) ∈ Atom1)))
36. signer(thr[i1]) = A ∈ Id
37. j : ℕi1
38. ↑thr[j] ∈b New
39. ↑isl(f signed(thr[i1]))
40. outl(f signed(thr[i1])) = New(thr[j]) ∈ Atom1
41. ∀k:{j + 1..i1-}
((↑thr[k] ∈b Sign) ⇒ (↑isl(f signed(thr[k]))) ⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1)))
42. thr2[j1] = thr[j] ∈ E
⊢ e1 = e2 ∈ E
BY
{ (Assert loc(thr[j]) = A ∈ Id BY
OnMaybeHyp 28 (\h. (Unfold `ses-thread-loc` h
THEN (InstHyp [⌜thr[j]⌝] h⋅ THENA Auto)
THEN All (Unfold `ses-thread`)
THEN Try (With ⌜j⌝ (D 0)⋅)
THEN Auto)))⋅ }
1
1. s : SES
2. ActionsDisjoint
3. PropertyO
4. PropertyS
5. bss : Basic1 List
6. f : SecurityData ⟶ (Atom1?)
7. A : Id@i
8. Honest(A)@i
9. ∀es:EO+(Info)
(Honest(A)
⇒ (∀e:Act
((loc(e) = A ∈ Id)
⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
∧ (∀thr1,thr2:Thread.
(e ∈ thr1
⇒ (thr1 is one of bss at A)
⇒ e ∈ thr2
⇒ (thr2 is one of bss at A)
⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))@i'
10. es : EO+(Info)@i'
11. E(Sign) ⊆r Act
12. ∀thr:Thread. ∀A:Id.
((thr is one of bss at A)
⇒ (∀i:ℕ||thr||
((↑thr[i] ∈b Sign)
⇒ ((signer(thr[i]) = A ∈ Id)
∧ (∃j:ℕi
((↑thr[j] ∈b New)
∧ (↑isl(f signed(thr[i])))
∧ (outl(f signed(thr[i])) = New(thr[j]) ∈ Atom1)
∧ (∀k:{j + 1..i-}
((↑thr[k] ∈b Sign)
⇒ (↑isl(f signed(thr[k])))
⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1))))))))))
13. e2 : E(Sign)@i
14. loc(e2) = A ∈ Id
15. thr2 : Thread
16. i : ℕ||thr2||
17. e2 = thr2[i] ∈ E
18. (thr2 is one of bss at A)
19. loc(thr2)= A
20. e1 : E(Sign)
21. Sign(e1) = Sign(e2) ∈ (SecurityData × Id × Atom1)
22. signer(e2) = A ∈ Id
23. signer(e1) = A ∈ Id
24. thr : Thread
25. i1 : ℕ||thr||
26. e1 = thr[i1] ∈ E
27. (thr is one of bss at A)
28. loc(thr)= A
29. ∀thr1,thr2:Thread.
(e1 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e1 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
30. signer(thr2[i]) = A ∈ Id
31. j1 : ℕi
32. ↑thr2[j1] ∈b New
33. ↑isl(f signed(thr2[i]))
34. outl(f signed(thr2[i])) = New(thr2[j1]) ∈ Atom1
35. ∀k:{j1 + 1..i-}
((↑thr2[k] ∈b Sign) ⇒ (↑isl(f signed(thr2[k]))) ⇒ (¬(outl(f signed(thr2[k])) = New(thr2[j1]) ∈ Atom1)))
36. signer(thr[i1]) = A ∈ Id
37. j : ℕi1
38. ↑thr[j] ∈b New
39. ↑isl(f signed(thr[i1]))
40. outl(f signed(thr[i1])) = New(thr[j]) ∈ Atom1
41. ∀k:{j + 1..i1-}
((↑thr[k] ∈b Sign) ⇒ (↑isl(f signed(thr[k]))) ⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1)))
42. thr2[j1] = thr[j] ∈ E
43. loc(thr[j]) = A ∈ Id
⊢ e1 = e2 ∈ E
Latex:
Latex:
1. s : SES
2. ActionsDisjoint
3. PropertyO
4. PropertyS
5. bss : Basic1 List
6. f : SecurityData {}\mrightarrow{} (Atom1?)
7. A : Id@i
8. Honest(A)@i
9. \mforall{}es:EO+(Info)
(Honest(A)
{}\mRightarrow{} (\mforall{}e:Act
((loc(e) = A)
{}\mRightarrow{} ((\mexists{}thr:Thread. (e \mmember{} thr \mwedge{} (thr is one of bss at A) \mwedge{} loc(thr)= A))
\mwedge{} (\mforall{}thr1,thr2:Thread.
(e \mmember{} thr1
{}\mRightarrow{} (thr1 is one of bss at A)
{}\mRightarrow{} e \mmember{} thr2
{}\mRightarrow{} (thr2 is one of bss at A)
{}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1)))))))@i'
10. es : EO+(Info)@i'
11. E(Sign) \msubseteq{}r Act
12. \mforall{}thr:Thread. \mforall{}A:Id.
((thr is one of bss at A)
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||thr||
((\muparrow{}thr[i] \mmember{}\msubb{} Sign)
{}\mRightarrow{} ((signer(thr[i]) = A)
\mwedge{} (\mexists{}j:\mBbbN{}i
((\muparrow{}thr[j] \mmember{}\msubb{} New)
\mwedge{} (\muparrow{}isl(f signed(thr[i])))
\mwedge{} (outl(f signed(thr[i])) = New(thr[j]))
\mwedge{} (\mforall{}k:\{j + 1..i\msupminus{}\}
((\muparrow{}thr[k] \mmember{}\msubb{} Sign)
{}\mRightarrow{} (\muparrow{}isl(f signed(thr[k])))
{}\mRightarrow{} (\mneg{}(outl(f signed(thr[k])) = New(thr[j])))))))))))
13. e2 : E(Sign)@i
14. loc(e2) = A
15. thr2 : Thread
16. i : \mBbbN{}||thr2||
17. e2 = thr2[i]
18. (thr2 is one of bss at A)
19. loc(thr2)= A
20. e1 : E(Sign)
21. Sign(e1) = Sign(e2)
22. signer(e2) = A
23. signer(e1) = A
24. thr : Thread
25. i1 : \mBbbN{}||thr||
26. e1 = thr[i1]
27. (thr is one of bss at A)
28. loc(thr)= A
29. \mforall{}thr1,thr2:Thread.
(e1 \mmember{} thr1
{}\mRightarrow{} (thr1 is one of bss at A)
{}\mRightarrow{} e1 \mmember{} thr2
{}\mRightarrow{} (thr2 is one of bss at A)
{}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1))
30. signer(thr2[i]) = A
31. j1 : \mBbbN{}i
32. \muparrow{}thr2[j1] \mmember{}\msubb{} New
33. \muparrow{}isl(f signed(thr2[i]))
34. outl(f signed(thr2[i])) = New(thr2[j1])
35. \mforall{}k:\{j1 + 1..i\msupminus{}\}
((\muparrow{}thr2[k] \mmember{}\msubb{} Sign)
{}\mRightarrow{} (\muparrow{}isl(f signed(thr2[k])))
{}\mRightarrow{} (\mneg{}(outl(f signed(thr2[k])) = New(thr2[j1]))))
36. signer(thr[i1]) = A
37. j : \mBbbN{}i1
38. \muparrow{}thr[j] \mmember{}\msubb{} New
39. \muparrow{}isl(f signed(thr[i1]))
40. outl(f signed(thr[i1])) = New(thr[j])
41. \mforall{}k:\{j + 1..i1\msupminus{}\}
((\muparrow{}thr[k] \mmember{}\msubb{} Sign) {}\mRightarrow{} (\muparrow{}isl(f signed(thr[k]))) {}\mRightarrow{} (\mneg{}(outl(f signed(thr[k])) = New(thr[j]))))
42. thr2[j1] = thr[j]
\mvdash{} e1 = e2
By
Latex:
(Assert loc(thr[j]) = A BY
OnMaybeHyp 28 (\mbackslash{}h. (Unfold `ses-thread-loc` h
THEN (InstHyp [\mkleeneopen{}thr[j]\mkleeneclose{}] h\mcdot{} THENA Auto)
THEN All (Unfold `ses-thread`)
THEN Try (With \mkleeneopen{}j\mkleeneclose{} (D 0)\mcdot{})
THEN Auto)))\mcdot{}
Home
Index