---

Step * 1 of Lemma fresh-sig-protocol1_property


1. s : SES
2. ActionsDisjoint
3. PropertyO
4. PropertyS
5. bss : Basic1 List
6. FreshSignatures(bss)
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 : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
13. (thr is one of bss at A)@i'
14. e1 : E(Sign)@i
15. e2 : E(Sign)@i
16. signature(e1) = signature(e2) ∈ Atom1@i
17. ∃i:ℕ||thr||. (e1 = thr[i] ∈ E)@i
⊢ e1 = e2 ∈ E
BY
{ (ExRepD
   THEN (FLemma `ses-signature-unique2` [-3] THENA Auto)
   THEN OnMaybeHyp 6 (\h. (Unfold `fresh-sig-protocol1` h
                           THEN ExRepD
                           THEN (InstHyp [⌈es⌉] (h+1)⋅ THENA Auto)
                           THEN Thin (h+1)
                           THEN PromoteHyp (-1) (-10)))
   THEN ((Assert signer(e1) = A ∈ Id BY
                OnMaybeHyp 11 (\h. (Unfold `ses-fresh-thread` h THEN InstHyp [⌈thr⌉;⌈A⌉;⌈i⌉] h⋅ THEN Complete (Auto))))
         THEN (Assert loc(e2) = A ∈ Id BY
                     OnMaybeHyp 4 (\h. (Unfold `ses-S` h
                                        THEN (InstHyp [⌈es⌉] h⋅ THENM D -1 THENM BHyp -2 )
                                        THEN Complete (Auto))))⋅
         THEN ((Assert ∃thr:Thread. (e2 ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A) BY
                      OnMaybeHyp 10 (\h. (RepUR ``ses-protocol1`` h
                                          THEN InstHyp [⌈es⌉;⌈e2⌉] h⋅
                                          THEN Auto
                                          THEN MemTypeCD
                                          THEN Auto
                                          THEN Sel 6 (D 0)
                                          THEN Auto)))
               THEN RenameTo `thr1' `thr'
               THEN ExRepD
               THEN RenameVar `thr2' (-4))⋅)⋅)⋅ }

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 = e2 ∈ E

---

Latex:

---

Latex:

1.  s  :  SES
2.  ActionsDisjoint
3.  PropertyO
4.  PropertyS
5.  bss  :  Basic1  List
6.  FreshSignatures(bss)
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.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\}  @i
13.  (thr  is  one  of  bss  at  A)@i'
14.  e1  :  E(Sign)@i
15.  e2  :  E(Sign)@i
16.  signature(e1)  =  signature(e2)@i
17.  \mexists{}i:\mBbbN{}||thr||.  (e1  =  thr[i])@i
\mvdash{}  e1  =  e2


By

---

Latex:
(ExRepD
  THEN  (FLemma  `ses-signature-unique2`  [-3]  THENA  Auto)
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (Unfold  `fresh-sig-protocol1`  h
                                                  THEN  ExRepD
                                                  THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  (h+1)\mcdot{}  THENA  Auto)
                                                  THEN  Thin  (h+1)
                                                  THEN  PromoteHyp  (-1)  (-10)))
  THEN  ((Assert  signer(e1)  =  A  BY
                            OnMaybeHyp  11  (\mbackslash{}h.  (Unfold  `ses-fresh-thread`  h
                                                                    THEN  InstHyp  [\mkleeneopen{}thr\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}
                                                                    THEN  Complete  (Auto))))
              THEN  (Assert  loc(e2)  =  A  BY
                                      OnMaybeHyp  4  (\mbackslash{}h.  (Unfold  `ses-S`  h
                                                                            THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  h\mcdot{}  THENM  D  -1  THENM  BHyp  -2  )
                                                                            THEN  Complete  (Auto))))\mcdot{}
              THEN  ((Assert  \mexists{}thr:Thread.  (e2  \mmember{}  thr  \mwedge{}  (thr  is  one  of  bss  at  A)  \mwedge{}  loc(thr)=  A)  BY
                                        OnMaybeHyp  10  (\mbackslash{}h.  (RepUR  ``ses-protocol1``  h
                                                                                THEN  InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]  h\mcdot{}
                                                                                THEN  Auto
                                                                                THEN  MemTypeCD
                                                                                THEN  Auto
                                                                                THEN  Sel  6  (D  0)
                                                                                THEN  Auto)))
                          THEN  RenameTo  `thr1'  `thr'
                          THEN  ExRepD
                          THEN  RenameVar  `thr2'  (-4))\mcdot{})\mcdot{})\mcdot{}

---

Home Index