---

Step * 1 1 2 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. 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
BY
{ (OnMaybeHyp 9 (\h. (RepUR ``ses-protocol1`` h
                      THEN (InstHyp [⌈es⌉;⌈e1⌉] h⋅ THENA (Auto THEN MemTypeCD THEN Auto THEN Sel 6 (D 0) THEN Auto))
                      ))
   THEN Auto
   THEN ExRepD)⋅ }

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. ∀es:EO+(Info)
     (Honest(A)
     ⇒ (∀e:Act
           ((loc(e) = A ∈ Id)
           ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
              ∧ (∀thr1,thr2:Thread.
                   (e ∈ thr1
                   ⇒ (thr1 is one of bss at A)
                   ⇒ e ∈ thr2
                   ⇒ (thr2 is one of bss at A)
                   ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))@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
24. thr : Thread
25. e1 ∈ thr
26. (thr is one of bss at A)
27. loc(thr)= A
28. ∀thr1,thr2:Thread.
      (e1 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e1 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
⊢ 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.  i  :  \mBbbN{}||thr2||
17.  e2  =  thr2[i]
18.  (thr2  is  one  of  bss  at  A)
19.  loc(thr2)=  A
20.  e1  :  E(Sign)
21.  Sign(e1)  =  Sign(e2)
22.  signer(e2)  =  A
23.  signer(e1)  =  A
\mvdash{}  e1  =  e2


By

---

Latex:
(OnMaybeHyp  9  (\mbackslash{}h.  (RepUR  ``ses-protocol1``  h
                                        THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]  h\mcdot{}
                                                    THENA  (Auto  THEN  MemTypeCD  THEN  Auto  THEN  Sel  6  (D  0)  THEN  Auto)
                                                    )
                                        ))
  THEN  Auto
  THEN  ExRepD)\mcdot{}

---

Home Index