---

Step * of Lemma ses-flow-axiom-ordering

∀s:SES. (ActionsDisjoint ⇒ PropertyF ⇒ PropertyO)
BY
{ ((Auto THEN (D 0 THENA Auto))
   THEN (InstLemma `ses-flow-has*` [⌜s⌝;⌜es⌝]⋅ THENA Auto)
   THEN (With ⌜es⌝ (D 3)⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast)
   THEN Try ((RepeatFor 2 (ParallelLast⋅) THEN Auto))
   THEN ((FHyp 4 [-2] ORELSE FHyp 4 [-1]) THENA Auto)
   THEN RepeatFor 2 ((ParallelLast THEN Auto))) }

1
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. ∀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'
6. ∀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'
7. ∀n:E(New). ∀e:E.  ((e has New(n)) ⇒ ses-flow(s;es;New(n);n;e))@i'
8. n : E(New)@i
9. ∀e:E. ((e has New(n)) ⇒ ses-flow(s;es;New(n);n;e))
10. e : E@i
11. (e has New(n))@i
12. ses-flow(s;es;New(n);n;e)
13. snd : E(Send)
14. n = snd ∈ E
15. (snd < e)
16. snd has* New(n)
⊢ (n <loc snd)

2
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(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'
7. ∀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'
8. e1 : E(Sign)@i
9. ∀b:E
     ((b has signature(e1))
     ⇒ (∃e2:E(Sign). ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(s;es;signature(e2);e2;b))))
10. b : E@i
11. (b has signature(e1))@i
12. e2 : E(Sign)
13. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
14. ses-flow(s;es;signature(e2);e2;b)
15. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
16. snd : E(Send)
17. e2 = snd ∈ E
18. (snd < b)
19. snd has* signature(e2)
⊢ (e2 <loc snd)

3
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(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'
7. ∀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'
8. e1 : E(Sign)@i
9. ∀b:E
     ((b has signature(e1))
     ⇒ (∃e2:E(Sign). ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(s;es;signature(e2);e2;b))))
10. b : E@i
11. (b has signature(e1))@i
12. e2 : E(Sign)
13. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
14. ses-flow(s;es;signature(e2);e2;b)
15. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
16. snd : E(Send)
17. e2 ≤loc snd 
18. (snd < b)
19. snd has* signature(e2)
20. (e2 <loc snd)
21. (snd < b)
⊢ snd has* signature(e1)

4
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)

5
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 ≤loc snd 
18. (snd < b)
19. snd has* cipherText(e2)
20. (e2 <loc snd)
21. (snd < b)
⊢ snd has* cipherText(e1)

---

Latex:

---

Latex:
\mforall{}s:SES.  (ActionsDisjoint  {}\mRightarrow{}  PropertyF  {}\mRightarrow{}  PropertyO)


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))
  THEN  (InstLemma  `ses-flow-has*`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}es\mkleeneclose{}  (D  3)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast)
  THEN  Try  ((RepeatFor  2  (ParallelLast\mcdot{})  THEN  Auto))
  THEN  ((FHyp  4  [-2]  ORELSE  FHyp  4  [-1])  THENA  Auto)
  THEN  RepeatFor  2  ((ParallelLast  THEN  Auto)))

---

Home Index