---

Step * 1 1 2 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. 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
28. e1 c≤ e2
⊢ e2 c≤ e1
BY
{ ((Assert (e1 has signature(e2)) BY
          (Sel 6 (D 0) THEN Auto THEN BLemma `ses-sign-has-atom` THEN Auto))
   THEN ((Assert ∃e3:E(Sign)
                  ((Sign(e3) = Sign(e2) ∈ (SecurityData × Id × Atom1))
                  ∧ (e3 ≤loc e1  ∨ (∃snd:E(Send). ((e3 <loc snd) ∧ (snd < e1) ∧ snd has* signature(e2))))) BY
                OnMaybeHyp 2 (\h. (Unfold `ses-ordering` h
                                   THEN InstHyp [⌈es⌉] h⋅
                                   THEN Auto
                                   THEN InstHyp [⌈e2⌉;⌈e1⌉] (-2)⋅
                                   THEN Complete (Auto))))
         THEN ExRepD
         THEN (Assert ⌈e3 = e2 ∈ E⌉⋅
               THENL [(ThinVar `e1' THEN ThinVar `thr1' THEN RenameVar `e1' (-2))
                     ; ((HypSubst (-1) (-2) THENA Auto) THEN D (-2) THEN ExRepD 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. 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

---

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.  e2  :  E(Sign)@i
17.  signature(e1)  =  signature(e2)@i
18.  i  :  \mBbbN{}||thr1||@i
19.  e1  =  thr1[i]@i
20.  signed(e1)  =  signed(e2)
21.  signer(e1)  =  signer(e2)
22.  signer(e1)  =  A
23.  loc(e2)  =  A
24.  thr2  :  Thread
25.  e2  \mmember{}  thr2
26.  (thr2  is  one  of  bss  at  A)
27.  loc(thr2)=  A
28.  e1  c\mleq{}  e2
\mvdash{}  e2  c\mleq{}  e1


By

---

Latex:
((Assert  (e1  has  signature(e2))  BY
                (Sel  6  (D  0)  THEN  Auto  THEN  BLemma  `ses-sign-has-atom`  THEN  Auto))
  THEN  ((Assert  \mexists{}e3:E(Sign)
                                ((Sign(e3)  =  Sign(e2))
                                \mwedge{}  (e3  \mleq{}loc  e1 
                                    \mvee{}  (\mexists{}snd:E(Send).  ((e3  <loc  snd)  \mwedge{}  (snd  <  e1)  \mwedge{}  snd  has*  signature(e2)))))  BY
                            OnMaybeHyp  2  (\mbackslash{}h.  (Unfold  `ses-ordering`  h
                                                                  THEN  InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  h\mcdot{}
                                                                  THEN  Auto
                                                                  THEN  InstHyp  [\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]  (-2)\mcdot{}
                                                                  THEN  Complete  (Auto))))
              THEN  ExRepD
              THEN  (Assert  \mkleeneopen{}e3  =  e2\mkleeneclose{}\mcdot{}
                          THENL  [(ThinVar  `e1'  THEN  ThinVar  `thr1'  THEN  RenameVar  `e1'  (-2))
                                      ;  ((HypSubst  (-1)  (-2)  THENA  Auto)  THEN  D  (-2)  THEN  ExRepD  THEN  Auto)\mcdot{}]
              ))\mcdot{}
  )\mcdot{}

---

Home Index