Step
*
1
1
1
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. thr1 : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr1 is one of bss at A)@i'
15. e1 : E(Sign)@i
16. i : ℕ||thr1||@i
17. e1 = thr1[i] ∈ E@i
18. signer(e1) = A ∈ Id
19. e2 : E(Sign)
20. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
21. signer(e2) = A ∈ Id
22. thr : Thread
23. i1 : ℕ||thr||
24. e2 = thr[i1] ∈ E
25. (thr is one of bss at A)
26. loc(thr)= A
27. ∀thr1,thr2:Thread.
(e2 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e2 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
28. signer(thr1[i]) = A ∈ Id
29. j1 : ℕi
30. ↑thr1[j1] ∈b New
31. ↑isl(f signed(thr1[i]))
32. outl(f signed(thr1[i])) = New(thr1[j1]) ∈ Atom1
33. ∀k:{j1 + 1..i-}
((↑thr1[k] ∈b Sign) ⇒ (↑isl(f signed(thr1[k]))) ⇒ (¬(outl(f signed(thr1[k])) = New(thr1[j1]) ∈ Atom1)))
34. signer(thr[i1]) = A ∈ Id
35. j : ℕi1
36. ↑thr[j] ∈b New
37. ↑isl(f signed(thr[i1]))
38. outl(f signed(thr[i1])) = New(thr[j]) ∈ Atom1
39. ∀k:{j + 1..i1-}
((↑thr[k] ∈b Sign) ⇒ (↑isl(f signed(thr[k]))) ⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1)))
40. thr1[j1] = thr[j] ∈ E
⊢ e2 = e1 ∈ E
BY
{ (Assert loc(thr[j]) = A ∈ Id BY
OnMaybeHyp 26 (\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. thr1 : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr1 is one of bss at A)@i'
15. e1 : E(Sign)@i
16. i : ℕ||thr1||@i
17. e1 = thr1[i] ∈ E@i
18. signer(e1) = A ∈ Id
19. e2 : E(Sign)
20. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
21. signer(e2) = A ∈ Id
22. thr : Thread
23. i1 : ℕ||thr||
24. e2 = thr[i1] ∈ E
25. (thr is one of bss at A)
26. loc(thr)= A
27. ∀thr1,thr2:Thread.
(e2 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e2 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
28. signer(thr1[i]) = A ∈ Id
29. j1 : ℕi
30. ↑thr1[j1] ∈b New
31. ↑isl(f signed(thr1[i]))
32. outl(f signed(thr1[i])) = New(thr1[j1]) ∈ Atom1
33. ∀k:{j1 + 1..i-}
((↑thr1[k] ∈b Sign) ⇒ (↑isl(f signed(thr1[k]))) ⇒ (¬(outl(f signed(thr1[k])) = New(thr1[j1]) ∈ Atom1)))
34. signer(thr[i1]) = A ∈ Id
35. j : ℕi1
36. ↑thr[j] ∈b New
37. ↑isl(f signed(thr[i1]))
38. outl(f signed(thr[i1])) = New(thr[j]) ∈ Atom1
39. ∀k:{j + 1..i1-}
((↑thr[k] ∈b Sign) ⇒ (↑isl(f signed(thr[k]))) ⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1)))
40. thr1[j1] = thr[j] ∈ E
41. loc(thr[j]) = A ∈ Id
⊢ e2 = e1 ∈ 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. thr1 : \{thr:Act List| \mforall{}i:\mBbbN{}||thr|| - 1. (thr[i] <loc thr[i + 1])\} @i
14. (thr1 is one of bss at A)@i'
15. e1 : E(Sign)@i
16. i : \mBbbN{}||thr1||@i
17. e1 = thr1[i]@i
18. signer(e1) = A
19. e2 : E(Sign)
20. Sign(e2) = Sign(e1)
21. signer(e2) = A
22. thr : Thread
23. i1 : \mBbbN{}||thr||
24. e2 = thr[i1]
25. (thr is one of bss at A)
26. loc(thr)= A
27. \mforall{}thr1,thr2:Thread.
(e2 \mmember{} thr1
{}\mRightarrow{} (thr1 is one of bss at A)
{}\mRightarrow{} e2 \mmember{} thr2
{}\mRightarrow{} (thr2 is one of bss at A)
{}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1))
28. signer(thr1[i]) = A
29. j1 : \mBbbN{}i
30. \muparrow{}thr1[j1] \mmember{}\msubb{} New
31. \muparrow{}isl(f signed(thr1[i]))
32. outl(f signed(thr1[i])) = New(thr1[j1])
33. \mforall{}k:\{j1 + 1..i\msupminus{}\}
((\muparrow{}thr1[k] \mmember{}\msubb{} Sign)
{}\mRightarrow{} (\muparrow{}isl(f signed(thr1[k])))
{}\mRightarrow{} (\mneg{}(outl(f signed(thr1[k])) = New(thr1[j1]))))
34. signer(thr[i1]) = A
35. j : \mBbbN{}i1
36. \muparrow{}thr[j] \mmember{}\msubb{} New
37. \muparrow{}isl(f signed(thr[i1]))
38. outl(f signed(thr[i1])) = New(thr[j])
39. \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]))))
40. thr1[j1] = thr[j]
\mvdash{} e2 = e1
By
Latex:
(Assert loc(thr[j]) = A BY
OnMaybeHyp 26 (\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