---

Step * 1 of Lemma ses-flow-has*


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

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)@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. 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. ∃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))

---

Latex:

---

Latex:

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\mleq{}  snd@i
9.  rcv  c\mleq{}  e2@i
10.  (snd  <  rcv)@i
11.  Send(snd)  =  Rcv(rcv)@i
12.  (e1  \mleq{}loc  snd    \mwedge{}  (snd  has  a))
\mvee{}  (\mexists{}snd@0:E(Send).  (e1  \mleq{}loc  snd@0    \mwedge{}  (snd@0  <  snd)  \mwedge{}  snd@0  has*  a))@i
13.  (rcv  \mleq{}loc  e2    \mwedge{}  (e2  has  a))  \mvee{}  (\mexists{}snd:E(Send).  (rcv  \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  -2

---

Home Index