Step
*
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. Protocol1(bss) A@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. 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. e2 : E(Sign)@i
17. signature(e1) = signature(e2) ∈ Atom1@i
18. i : ℕ||thr1||@i
19. e1 = thr1[i] ∈ E@i
20. signed(e1) = signed(e2) ∈ SecurityData
21. signer(e1) = signer(e2) ∈ Id
22. signer(e1) = A ∈ Id
23. loc(e2) = A ∈ Id
24. thr2 : Thread
25. e2 ∈ thr2
26. (thr2 is one of bss at A)
27. loc(thr2)= A
⊢ e1 = e2 ∈ E
BY
{ (Assert ⌈e1 c≤ e2 ∧ e2 c≤ e1⌉⋅ 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. Protocol1(bss) A@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. 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. e2 : E(Sign)@i
17. signature(e1) = signature(e2) ∈ Atom1@i
18. i : ℕ||thr1||@i
19. e1 = thr1[i] ∈ E@i
20. signed(e1) = signed(e2) ∈ SecurityData
21. signer(e1) = signer(e2) ∈ Id
22. signer(e1) = A ∈ Id
23. loc(e2) = A ∈ Id
24. thr2 : Thread
25. e2 ∈ thr2
26. (thr2 is one of bss at A)
27. loc(thr2)= A
⊢ e1 c≤ e2
2
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. Protocol1(bss) A@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. 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. e2 : E(Sign)@i
17. signature(e1) = signature(e2) ∈ Atom1@i
18. i : ℕ||thr1||@i
19. e1 = thr1[i] ∈ E@i
20. signed(e1) = signed(e2) ∈ SecurityData
21. signer(e1) = signer(e2) ∈ Id
22. signer(e1) = A ∈ Id
23. loc(e2) = A ∈ Id
24. thr2 : Thread
25. e2 ∈ thr2
26. (thr2 is one of bss at A)
27. loc(thr2)= A
28. e1 c≤ e2
⊢ e2 c≤ e1
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. Protocol1(bss) A@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. 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. e2 : E(Sign)@i
17. signature(e1) = signature(e2)@i
18. i : \mBbbN{}||thr1||@i
19. e1 = thr1[i]@i
20. signed(e1) = signed(e2)
21. signer(e1) = signer(e2)
22. signer(e1) = A
23. loc(e2) = A
24. thr2 : Thread
25. e2 \mmember{} thr2
26. (thr2 is one of bss at A)
27. loc(thr2)= A
\mvdash{} e1 = e2
By
Latex:
(Assert \mkleeneopen{}e1 c\mleq{} e2 \mwedge{} e2 c\mleq{} e1\mkleeneclose{}\mcdot{} THEN Auto)\mcdot{}
Home
Index