---

Step * 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. 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. 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)
⊢ e2 = e1 ∈ E
BY
{ (Assert signer(e2) = A ∈ Id BY
         (All (Unfold `ses-signer`) 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. 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
⊢ 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.  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.  i  :  \mBbbN{}||thr1||@i
17.  e1  =  thr1[i]@i
18.  signer(e1)  =  A
19.  e2  :  E(Sign)
20.  Sign(e2)  =  Sign(e1)
\mvdash{}  e2  =  e1


By

---

Latex:
(Assert  signer(e2)  =  A  BY
              (All  (Unfold  `ses-signer`)  THEN  Auto))

---

Home Index