Step
*
1
1
2
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) ⇒ ses-fresh-thread(s;es;f;A;thr))
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. e1 ∈ thr
26. (thr is one of bss at A)
27. loc(thr)= A
28. ∀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))
⊢ e1 = e2 ∈ E
BY
{ (D -4
THEN Unfold `ses-fresh-thread` 12
THEN (InstHyp [⌜thr2⌝;⌜A⌝;⌜i⌝] 12⋅ THENA (Try (QuickAuto) THEN DVar `e2' THEN Unhide THEN Auto))
THEN (InstHyp [⌜thr⌝;⌜A⌝;⌜i1⌝] 12⋅ THENA (Try (QuickAuto) THEN DVar `e1' THEN Unhide THEN Auto))
THEN Auto
THEN ExRepD)⋅ }
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)))
⊢ 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{} ses-fresh-thread(s;es;f;A;thr))
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. e1 \mmember{} thr
26. (thr is one of bss at A)
27. loc(thr)= A
28. \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))
\mvdash{} e1 = e2
By
Latex:
(D -4
THEN Unfold `ses-fresh-thread` 12
THEN (InstHyp [\mkleeneopen{}thr2\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}] 12\mcdot{} THENA (Try (QuickAuto) THEN DVar `e2' THEN Unhide THEN Auto))
THEN (InstHyp [\mkleeneopen{}thr\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i1\mkleeneclose{}] 12\mcdot{} THENA (Try (QuickAuto) THEN DVar `e1' THEN Unhide THEN Auto))
THEN Auto
THEN ExRepD)\mcdot{}
Home
Index