---

Step * 2 of Lemma ses-flow-has*


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))
BY
{ D (-3) }

1
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)@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))

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. ∃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:

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\mleq{}  e2@i
10.  (encr  <  decr)@i
11.  plainText(decr)  =  plainText(encr)@i
12.  cipherText(decr)  =  cipherText(encr)@i
13.  MatchingKeys(key(decr);key(encr))@i
14.  \mneg{}(key(decr)  =  symmetric-key(a))@i
15.  (e1  \mleq{}loc  encr    \mwedge{}  (encr  has  a))  \mvee{}  (\mexists{}snd:E(Send).  (e1  \mleq{}loc  snd    \mwedge{}  (snd  <  encr)  \mwedge{}  snd  has*  a))@i
16.  (encr  \mleq{}loc  decr    \mwedge{}  (decr  has  cipherText(encr)))
\mvee{}  (\mexists{}snd:E(Send).  (encr  \mleq{}loc  snd    \mwedge{}  (snd  <  decr)  \mwedge{}  snd  has*  cipherText(encr)))@i
17.  (decr  \mleq{}loc  e2    \mwedge{}  (e2  has  a))  \mvee{}  (\mexists{}snd:E(Send).  (decr  \mleq{}loc  snd    \mwedge{}  (snd  <  e2)  \mwedge{}  snd  has*  a))@i
\mvdash{}  (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:
D  (-3)

---

Home Index