---

Step * 1 1 1 1 1 of Lemma signature-release-lemma


1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyF
5. PropertyO
6. ses-ordering'(ses)
7. PropertyN
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. UniqueSignatures(bss)
16. A : Id
17. Honest(A)
18. Protocol1(bss) A
19. es : EO+(Info)
20. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
21. (thr is one of bss at A)
22. loc(thr)= A
23. i : ℕ||thr||
24. j : ℕi
25. ↑thr[j] ∈b Sign
26. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
27. loc(thr[j]) = A ∈ Id
28. loc(thr[i]) = A ∈ Id
29. e : E@i
30. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* signature(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈b Send)))))
31. Action(e)@i
32. e has* signature(thr[j])@i
⊢ ((¬(loc(e) = A ∈ Id)) ⇒ (thr[i] < e)) ∧ ((e <loc thr[i]) ⇒ (e ∈ thr ∧ (¬↑e ∈b Send)))
BY
{ ((Assert ∃e2:E(Sign)
            ((Sign(e2) = Sign(thr[j]) ∈ (SecurityData × Id × Atom1))
            ∧ (e2 ≤loc e  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < e) ∧ snd has* signature(thr[j]))))) BY
          OnMaybeHyp 6 (\h. (Unfold `ses-ordering\'` h
                             THEN (InstHyp [⌈es⌉;⌈e⌉] h⋅ THENA Auto)
                             THEN ExRepD
                             THEN InstHyp [⌈thr[j]⌉] (-2)⋅
                             THEN Auto)))⋅
   THEN ExRepD
   ) }

1
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyF
5. PropertyO
6. ses-ordering'(ses)
7. PropertyN
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. UniqueSignatures(bss)
16. A : Id
17. Honest(A)
18. Protocol1(bss) A
19. es : EO+(Info)
20. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
21. (thr is one of bss at A)
22. loc(thr)= A
23. i : ℕ||thr||
24. j : ℕi
25. ↑thr[j] ∈b Sign
26. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
27. loc(thr[j]) = A ∈ Id
28. loc(thr[i]) = A ∈ Id
29. e : E@i
30. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* signature(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈b Send)))))
31. Action(e)@i
32. e has* signature(thr[j])@i
33. e2 : E(Sign)
34. Sign(e2) = Sign(thr[j]) ∈ (SecurityData × Id × Atom1)
35. e2 ≤loc e  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < e) ∧ snd has* signature(thr[j])))
⊢ ((¬(loc(e) = A ∈ Id)) ⇒ (thr[i] < e)) ∧ ((e <loc thr[i]) ⇒ (e ∈ thr ∧ (¬↑e ∈b Send)))

---

Latex:

---

Latex:

1.  ses  :  SES
2.  ActionsDisjoint
3.  NoncesCiphersAndKeysDisjoint
4.  PropertyF
5.  PropertyO
6.  ses-ordering'(ses)
7.  PropertyN
8.  PropertyV
9.  PropertyR
10.  PropertyD
11.  PropertyS
12.  PropertyK
13.  bss  :  Basic1  List
14.  Legal(bss)
15.  UniqueSignatures(bss)
16.  A  :  Id
17.  Honest(A)
18.  Protocol1(bss)  A
19.  es  :  EO+(Info)
20.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\} 
21.  (thr  is  one  of  bss  at  A)
22.  loc(thr)=  A
23.  i  :  \mBbbN{}||thr||
24.  j  :  \mBbbN{}i
25.  \muparrow{}thr[j]  \mmember{}\msubb{}  Sign
26.  \mforall{}k:\{j  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}thr[k]  \mmember{}\msubb{}  Send)
27.  loc(thr[j])  =  A
28.  loc(thr[i])  =  A
29.  e  :  E@i
30.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  Action(e1)
            {}\mRightarrow{}  e1  has*  signature(thr[j])
            {}\mRightarrow{}  (((\mneg{}(loc(e1)  =  A))  {}\mRightarrow{}  (thr[i]  <  e1))  \mwedge{}  ((e1  <loc  thr[i])  {}\mRightarrow{}  (e1  \mmember{}  thr  \mwedge{}  (\mneg{}\muparrow{}e1  \mmember{}\msubb{}  Send)))))
31.  Action(e)@i
32.  e  has*  signature(thr[j])@i
\mvdash{}  ((\mneg{}(loc(e)  =  A))  {}\mRightarrow{}  (thr[i]  <  e))  \mwedge{}  ((e  <loc  thr[i])  {}\mRightarrow{}  (e  \mmember{}  thr  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)))


By

---

Latex:
((Assert  \mexists{}e2:E(Sign)
                    ((Sign(e2)  =  Sign(thr[j]))
                    \mwedge{}  (e2  \mleq{}loc  e 
                        \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  e)  \mwedge{}  snd  has*  signature(thr[j])))))  BY
                OnMaybeHyp  6  (\mbackslash{}h.  (Unfold  `ses-ordering\mbackslash{}'`  h
                                                      THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                                      THEN  ExRepD
                                                      THEN  InstHyp  [\mkleeneopen{}thr[j]\mkleeneclose{}]  (-2)\mcdot{}
                                                      THEN  Auto)))\mcdot{}
  THEN  ExRepD
  )

---

Home Index