---

Step * 1 2 1 1 1 3 of Lemma ses-ordering-ordering'


1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕm. ∀b:E.
     ((∀n:E(New). ∀e':E.
         (((e' has New(n)) ∧ (e' ->>^m b))
         ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
     ∧ (∀e1:E(Sign). ∀e':E.
          (((e' has signature(e1)) ∧ (e' ->>^m b))
          ⇒ (∃e2:E(Sign)
               ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
               ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))))))))
     ∧ (∀e1:E(Encrypt). ∀e':E.
          (((e' has cipherText(e1)) ∧ (e' ->>^m b))
          ⇒ (∃e2:E(Encrypt)
               ((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
               ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))))@i
7. b : E@i
8. ∀n:E(New). ∀e':E.
     (((e' has New(n)) ∧ (e' ->>^m b)) ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(z)))
20. same-action(z;e2)
21. ∃e3:E(Sign)
     ((Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1))
     ∧ (e3 ≤loc e2  ∨ (∃snd:E(Send). ((e3 <loc snd) ∧ (snd < e2) ∧ snd has* signature(e1)))))
⊢ ∃e2:E(Sign)
   ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
   ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1)))))
BY
{ (ParallelLast THEN Auto THEN Decide e3 ≤loc b ⋅ THEN Auto)⋅ }

1
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. m : ℕ
6. ∀m:ℕm. ∀b:E.
     ((∀n:E(New). ∀e':E.
         (((e' has New(n)) ∧ (e' ->>^m b))
         ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
     ∧ (∀e1:E(Sign). ∀e':E.
          (((e' has signature(e1)) ∧ (e' ->>^m b))
          ⇒ (∃e2:E(Sign)
               ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
               ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))))))))
     ∧ (∀e1:E(Encrypt). ∀e':E.
          (((e' has cipherText(e1)) ∧ (e' ->>^m b))
          ⇒ (∃e2:E(Encrypt)
               ((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
               ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))))@i
7. b : E@i
8. ∀n:E(New). ∀e':E.
     (((e' has New(n)) ∧ (e' ->>^m b)) ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n)))))
9. e1 : E(Sign)@i
10. e' : E@i
11. (e' has signature(e1))@i
12. z : E
13. 0 < m
14. e' ->>^m - 1 z
15. ↑z ∈b Encrypt
16. (b has cipherText(z))
17. e2 : E(Encrypt)
18. Encrypt(e2) = Encrypt(z) ∈ (SecurityData × Key × Atom1)
19. e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(z)))
20. same-action(z;e2)
21. e3 : E(Sign)
22. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
23. e3 ≤loc e2  ∨ (∃snd:E(Send). ((e3 <loc snd) ∧ (snd < e2) ∧ snd has* signature(e1)))
24. Sign(e3) = Sign(e1) ∈ (SecurityData × Id × Atom1)
25. ¬e3 ≤loc b 
⊢ ∃snd:E(Send). ((e3 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  PropertyO@i'
3.  ActionsDisjoint@i'
4.  es  :  EO+(Info)@i'
5.  m  :  \mBbbN{}
6.  \mforall{}m:\mBbbN{}m.  \mforall{}b:E.
          ((\mforall{}n:E(New).  \mforall{}e':E.
                  (((e'  has  New(n))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
                  {}\mRightarrow{}  (n  \mleq{}loc  b    \mvee{}  (\mexists{}snd:E(Send).  ((n  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  New(n))))))
          \mwedge{}  (\mforall{}e1:E(Sign).  \mforall{}e':E.
                    (((e'  has  signature(e1))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
                    {}\mRightarrow{}  (\mexists{}e2:E(Sign)
                              ((Sign(e2)  =  Sign(e1))
                              \mwedge{}  (e2  \mleq{}loc  b 
                                  \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  signature(e1))))))))
          \mwedge{}  (\mforall{}e1:E(Encrypt).  \mforall{}e':E.
                    (((e'  has  cipherText(e1))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
                    {}\mRightarrow{}  (\mexists{}e2:E(Encrypt)
                              ((Encrypt(e2)  =  Encrypt(e1))
                              \mwedge{}  (e2  \mleq{}loc  b 
                                  \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  cipherText(e1)))))))))@i
7.  b  :  E@i
8.  \mforall{}n:E(New).  \mforall{}e':E.
          (((e'  has  New(n))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
          {}\mRightarrow{}  (n  \mleq{}loc  b    \mvee{}  (\mexists{}snd:E(Send).  ((n  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  New(n)))))
9.  e1  :  E(Sign)@i
10.  e'  :  E@i
11.  (e'  has  signature(e1))@i
12.  z  :  E
13.  0  <  m
14.  e'  rel\_exp(E;  ->>  m  -  1)  z
15.  \muparrow{}z  \mmember{}\msubb{}  Encrypt
16.  (b  has  cipherText(z))
17.  e2  :  E(Encrypt)
18.  Encrypt(e2)  =  Encrypt(z)
19.  e2  \mleq{}loc  b    \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  cipherText(z)))
20.  same-action(z;e2)
21.  \mexists{}e3:E(Sign)
          ((Sign(e3)  =  Sign(e1))
          \mwedge{}  (e3  \mleq{}loc  e2    \mvee{}  (\mexists{}snd:E(Send).  ((e3  <loc  snd)  \mwedge{}  (snd  <  e2)  \mwedge{}  snd  has*  signature(e1)))))
\mvdash{}  \mexists{}e2:E(Sign)
      ((Sign(e2)  =  Sign(e1))
      \mwedge{}  (e2  \mleq{}loc  b    \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  signature(e1)))))


By

---

Latex:
(ParallelLast  THEN  Auto  THEN  Decide  e3  \mleq{}loc  b  \mcdot{}  THEN  Auto)\mcdot{}

---

Home Index