---

Step * 1 1 2 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. e2 : E(Sign)@i
14. loc(e2) = A ∈ Id
15. thr2 : Thread
16. e2 ∈ thr2
17. (thr2 is one of bss at A)
18. loc(thr2)= A
19. e1 : E(Sign)
20. Sign(e1) = Sign(e2) ∈ (SecurityData × Id × Atom1)
⊢ e1 = e2 ∈ E
BY
{ (D -5
   THEN (Assert signer(e2) = A ∈ Id BY
               (Unfold `ses-fresh-thread` 12
                THEN InstHyp [⌈thr2⌉;⌈A⌉;⌈i⌉] 12⋅
                THEN Try (QuickAuto)
                THEN DVar `e2'
                THEN Unhide
                THEN Auto))
   THEN (Assert signer(e1) = 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. 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
⊢ 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.  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.  e2  :  E(Sign)@i
14.  loc(e2)  =  A
15.  thr2  :  Thread
16.  e2  \mmember{}  thr2
17.  (thr2  is  one  of  bss  at  A)
18.  loc(thr2)=  A
19.  e1  :  E(Sign)
20.  Sign(e1)  =  Sign(e2)
\mvdash{}  e1  =  e2


By

---

Latex:
(D  -5
  THEN  (Assert  signer(e2)  =  A  BY
                          (Unfold  `ses-fresh-thread`  12
                            THEN  InstHyp  [\mkleeneopen{}thr2\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  12\mcdot{}
                            THEN  Try  (QuickAuto)
                            THEN  DVar  `e2'
                            THEN  Unhide
                            THEN  Auto))
  THEN  (Assert  signer(e1)  =  A  BY
                          (All  (Unfold  `ses-signer`)  THEN  Auto)))

---

Home Index