---

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