---

Step * of Lemma fresh-sig-protocol1_property

∀[s:SES]
  (∀[bss:Basic1 List]. UniqueSignatures(bss) supposing FreshSignatures(bss)) supposing 
     (PropertyS and 
     PropertyO and 
     ActionsDisjoint)
BY
{ (BasicUniformUnivCD Auto
   THEN RepeatFor 4 ((D 0 THENA Auto))
   THEN (Assert E(Sign) ⊆r Act BY
               ((D 0 THEN Auto) THEN MemTypeCD THEN Auto THEN Sel 6 (D 0) THEN Auto))
   THEN Auto
   THEN D 0
   THEN Auto
   THEN All (Unfolds ``ses-thread ses-thread-member``)) }

1
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

---

Latex:

---

Latex:
\mforall{}[s:SES]
    (\mforall{}[bss:Basic1  List].  UniqueSignatures(bss)  supposing  FreshSignatures(bss))  supposing 
          (PropertyS  and 
          PropertyO  and 
          ActionsDisjoint)


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (Assert  E(Sign)  \msubseteq{}r  Act  BY
                          ((D  0  THEN  Auto)  THEN  MemTypeCD  THEN  Auto  THEN  Sel  6  (D  0)  THEN  Auto))
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  All  (Unfolds  ``ses-thread  ses-thread-member``))

---

Home Index