---

Step * 4 of Lemma ses-flow-axiom-ordering


1. s : SES@i'
2. ActionsDisjoint@i'
3. es : EO+(Info)@i'
4. ∀e1,e2:E. ∀a:Atom1.
     (ses-flow(s;es;a;e1;e2) ⇒ ((e1 ≤loc e2  ∧ (e2 has a)) ∨ (∃snd:E(Send). (e1 ≤loc snd  ∧ (snd < e2) ∧ snd has* a))))
5. ∀n:E(New). ∀e:E.  ((e has New(n)) ⇒ ses-flow(s;es;New(n);n;e))@i'
6. ∀e1:E(Sign). ∀b:E.
     ((b has signature(e1))
     ⇒ (∃e2:E(Sign). ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(s;es;signature(e2);e2;b))))@i'
7. ∀e1:E(Encrypt). ∀b:E.
     ((b has cipherText(e1))
     ⇒ (∃e2:E(Encrypt)
          ((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1)) ∧ ses-flow(s;es;cipherText(e2);e2;b))))@i'
8. e1 : E(Encrypt)@i
9. ∀b:E
     ((b has cipherText(e1))
     ⇒ (∃e2:E(Encrypt)
          ((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1)) ∧ ses-flow(s;es;cipherText(e2);e2;b))))
10. b : E@i
11. (b has cipherText(e1))@i
12. e2 : E(Encrypt)
13. Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1)
14. ses-flow(s;es;cipherText(e2);e2;b)
15. Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1)
16. snd : E(Send)
17. e2 = snd ∈ E
18. (snd < b)
19. snd has* cipherText(e2)
⊢ (e2 <loc snd)
BY
{ ((Assert (↑e2 ∈b Encrypt) ∧ (↑e2 ∈b Send) BY
          Auto)
   THEN ((With ⌈es⌉ (D 2)⋅ THENM D -1) THENA Auto)
   THEN InstHyp [⌈e2⌉] (-1)⋅
   THEN Auto
   THEN ThinTrivial
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  es  :  EO+(Info)@i'
4.  \mforall{}e1,e2:E.  \mforall{}a:Atom1.
          (ses-flow(s;es;a;e1;e2)
          {}\mRightarrow{}  ((e1  \mleq{}loc  e2    \mwedge{}  (e2  has  a))  \mvee{}  (\mexists{}snd:E(Send).  (e1  \mleq{}loc  snd    \mwedge{}  (snd  <  e2)  \mwedge{}  snd  has*  a))))
5.  \mforall{}n:E(New).  \mforall{}e:E.    ((e  has  New(n))  {}\mRightarrow{}  ses-flow(s;es;New(n);n;e))@i'
6.  \mforall{}e1:E(Sign).  \mforall{}b:E.
          ((b  has  signature(e1))
          {}\mRightarrow{}  (\mexists{}e2:E(Sign).  ((Sign(e2)  =  Sign(e1))  \mwedge{}  ses-flow(s;es;signature(e2);e2;b))))@i'
7.  \mforall{}e1:E(Encrypt).  \mforall{}b:E.
          ((b  has  cipherText(e1))
          {}\mRightarrow{}  (\mexists{}e2:E(Encrypt).  ((Encrypt(e2)  =  Encrypt(e1))  \mwedge{}  ses-flow(s;es;cipherText(e2);e2;b))))@i'
8.  e1  :  E(Encrypt)@i
9.  \mforall{}b:E
          ((b  has  cipherText(e1))
          {}\mRightarrow{}  (\mexists{}e2:E(Encrypt).  ((Encrypt(e2)  =  Encrypt(e1))  \mwedge{}  ses-flow(s;es;cipherText(e2);e2;b))))
10.  b  :  E@i
11.  (b  has  cipherText(e1))@i
12.  e2  :  E(Encrypt)
13.  Encrypt(e2)  =  Encrypt(e1)
14.  ses-flow(s;es;cipherText(e2);e2;b)
15.  Encrypt(e2)  =  Encrypt(e1)
16.  snd  :  E(Send)
17.  e2  =  snd
18.  (snd  <  b)
19.  snd  has*  cipherText(e2)
\mvdash{}  (e2  <loc  snd)


By

---

Latex:
((Assert  (\muparrow{}e2  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (\muparrow{}e2  \mmember{}\msubb{}  Send)  BY
                Auto)
  THEN  ((With  \mkleeneopen{}es\mkleeneclose{}  (D  2)\mcdot{}  THENM  D  -1)  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}e2\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  ThinTrivial
  THEN  Auto)\mcdot{}

---

Home Index