---

Step * 1 2 of Lemma ses-flow-implies'


1. s : SES@i'
2. es : EO+(Info)@i'
3. [P] : E ─→ E ─→ Atom1 ─→ ℙ
4. ∀e1,e2:E. ∀a:Atom1.  (((e1 has a) ∧ (e2 has a) ∧ e1 ≤loc e2 ) ⇒ P[e1;e2;a])@i
5. ∀e1,e2:E. ∀snd:E(Send). ∀rcv:E(Rcv). ∀a:Atom1.
     ((e1 c≤ snd
     ∧ rcv c≤ e2
     ∧ (snd < rcv)
     ∧ (Send(snd) = Rcv(rcv) ∈ SecurityData)
     ∧ (P[e1;snd;a] ∧ ses-flow(s;es;a;e1;snd))
     ∧ P[rcv;e2;a]
     ∧ ses-flow(s;es;a;rcv;e2))
     ⇒ P[e1;e2;a])@i
6. ∀e1,e2:E. ∀encr:E(Encrypt). ∀decr:E(Decrypt). ∀a:Atom1.
     (((e1 <loc encr)
     ∧ decr c≤ e2
     ∧ (encr < decr)
     ∧ ((plainText(decr) = plainText(encr) ∈ SecurityData)
       ∧ (cipherText(decr) = cipherText(encr) ∈ Atom1)
       ∧ MatchingKeys(key(decr);key(encr)))
     ∧ (¬(key(decr) = symmetric-key(a) ∈ Key))
     ∧ (P[e1;encr;a] ∧ ses-flow(s;es;a;e1;encr))
     ∧ (P[encr;decr;cipherText(encr)] ∧ ses-flow(s;es;cipherText(encr);encr;decr))
     ∧ P[decr;e2;a]
     ∧ ses-flow(s;es;a;decr;e2))
     ⇒ P[e1;e2;a])@i
7. e1 : E@i
8. e2 : E@i
9. ∀x,y:E.  (e1 c≤ x ⇒ x c≤ y ⇒ y c≤ e2 ⇒ ((e1 < x) ∨ (y < e2)) ⇒ (∀a:Atom1. (ses-flow(s;es;a;x;y) ⇒ P[x;y;a])))@i
10. a : Atom1@i
11. snd : E(Send)@i
12. rcv : E(Rcv)@i
13. e1 c≤ snd@i
14. rcv c≤ e2@i
15. (snd < rcv)@i
16. Send(snd) = Rcv(rcv) ∈ SecurityData@i
17. ses-flow(s;es;a;e1;snd)@i
18. ses-flow(s;es;a;rcv;e2)@i
⊢ P[e1;e2;a]
BY
{ (InstHyp [⌈e1⌉;⌈e2⌉;⌈snd⌉;⌈rcv⌉;⌈a⌉] 5⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  [P]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}e1,e2:E.  \mforall{}a:Atom1.    (((e1  has  a)  \mwedge{}  (e2  has  a)  \mwedge{}  e1  \mleq{}loc  e2  )  {}\mRightarrow{}  P[e1;e2;a])@i
5.  \mforall{}e1,e2:E.  \mforall{}snd:E(Send).  \mforall{}rcv:E(Rcv).  \mforall{}a:Atom1.
          ((e1  c\mleq{}  snd
          \mwedge{}  rcv  c\mleq{}  e2
          \mwedge{}  (snd  <  rcv)
          \mwedge{}  (Send(snd)  =  Rcv(rcv))
          \mwedge{}  (P[e1;snd;a]  \mwedge{}  ses-flow(s;es;a;e1;snd))
          \mwedge{}  P[rcv;e2;a]
          \mwedge{}  ses-flow(s;es;a;rcv;e2))
          {}\mRightarrow{}  P[e1;e2;a])@i
6.  \mforall{}e1,e2:E.  \mforall{}encr:E(Encrypt).  \mforall{}decr:E(Decrypt).  \mforall{}a:Atom1.
          (((e1  <loc  encr)
          \mwedge{}  decr  c\mleq{}  e2
          \mwedge{}  (encr  <  decr)
          \mwedge{}  ((plainText(decr)  =  plainText(encr))
              \mwedge{}  (cipherText(decr)  =  cipherText(encr))
              \mwedge{}  MatchingKeys(key(decr);key(encr)))
          \mwedge{}  (\mneg{}(key(decr)  =  symmetric-key(a)))
          \mwedge{}  (P[e1;encr;a]  \mwedge{}  ses-flow(s;es;a;e1;encr))
          \mwedge{}  (P[encr;decr;cipherText(encr)]  \mwedge{}  ses-flow(s;es;cipherText(encr);encr;decr))
          \mwedge{}  P[decr;e2;a]
          \mwedge{}  ses-flow(s;es;a;decr;e2))
          {}\mRightarrow{}  P[e1;e2;a])@i
7.  e1  :  E@i
8.  e2  :  E@i
9.  \mforall{}x,y:E.
          (e1  c\mleq{}  x
          {}\mRightarrow{}  x  c\mleq{}  y
          {}\mRightarrow{}  y  c\mleq{}  e2
          {}\mRightarrow{}  ((e1  <  x)  \mvee{}  (y  <  e2))
          {}\mRightarrow{}  (\mforall{}a:Atom1.  (ses-flow(s;es;a;x;y)  {}\mRightarrow{}  P[x;y;a])))@i
10.  a  :  Atom1@i
11.  snd  :  E(Send)@i
12.  rcv  :  E(Rcv)@i
13.  e1  c\mleq{}  snd@i
14.  rcv  c\mleq{}  e2@i
15.  (snd  <  rcv)@i
16.  Send(snd)  =  Rcv(rcv)@i
17.  ses-flow(s;es;a;e1;snd)@i
18.  ses-flow(s;es;a;rcv;e2)@i
\mvdash{}  P[e1;e2;a]


By

---

Latex:
(InstHyp  [\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}snd\mkleeneclose{};\mkleeneopen{}rcv\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  5\mcdot{}  THEN  Auto)

---

Home Index