---

Step * of Lemma ses-flow-has*

∀s:SES. ∀es:EO+(Info). ∀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))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN BLemma `ses-flow-implies` THEN Auto) }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. snd : E(Send)@i
6. rcv : E(Rcv)@i
7. a : Atom1@i
8. e1 c≤ snd@i
9. rcv c≤ e2@i
10. (snd < rcv)@i
11. Send(snd) = Rcv(rcv) ∈ SecurityData@i
12. (e1 ≤loc snd  ∧ (snd has a)) ∨ (∃snd@0:E(Send). (e1 ≤loc snd@0  ∧ (snd@0 < snd) ∧ snd@0 has* a))@i
13. (rcv ≤loc e2  ∧ (e2 has a)) ∨ (∃snd:E(Send). (rcv ≤loc snd  ∧ (snd < e2) ∧ snd has* a))@i
⊢ (e1 ≤loc e2  ∧ (e2 has a)) ∨ (∃snd:E(Send). (e1 ≤loc snd  ∧ (snd < e2) ∧ snd has* a))

2
1. s : SES@i'
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. encr : E(Encrypt)@i
6. decr : E(Decrypt)@i
7. a : Atom1@i
8. (e1 <loc encr)@i
9. decr c≤ e2@i
10. (encr < decr)@i
11. plainText(decr) = plainText(encr) ∈ SecurityData@i
12. cipherText(decr) = cipherText(encr) ∈ Atom1@i
13. MatchingKeys(key(decr);key(encr))@i
14. ¬(key(decr) = symmetric-key(a) ∈ Key)@i
15. (e1 ≤loc encr  ∧ (encr has a)) ∨ (∃snd:E(Send). (e1 ≤loc snd  ∧ (snd < encr) ∧ snd has* a))@i
16. (encr ≤loc decr  ∧ (decr has cipherText(encr)))
∨ (∃snd:E(Send). (encr ≤loc snd  ∧ (snd < decr) ∧ snd has* cipherText(encr)))@i
17. (decr ≤loc e2  ∧ (e2 has a)) ∨ (∃snd:E(Send). (decr ≤loc snd  ∧ (snd < e2) ∧ snd has* a))@i
⊢ (e1 ≤loc e2  ∧ (e2 has a)) ∨ (∃snd:E(Send). (e1 ≤loc snd  ∧ (snd < e2) ∧ snd has* a))

---

Latex:

---

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).  \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))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  BLemma  `ses-flow-implies`  THEN  Auto)

---

Home Index