---

Step * 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,e2:E. ∀a:Atom1.  (ses-flow(s;es;a;e1;e2) ⇒ P[e1;e2;a])
⊢ {∀e1,e2:E. ∀a:Atom1.  (ses-flow(s;es;a;e1;e2) ⇒ P[e1;e2;a])}
BY
{ (Unfold `guard` 0 THEN Trivial) }

---

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.  \mforall{}e1,e2:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;e1;e2)  {}\mRightarrow{}  P[e1;e2;a])
\mvdash{}  \{\mforall{}e1,e2:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;e1;e2)  {}\mRightarrow{}  P[e1;e2;a])\}


By

---

Latex:
(Unfold  `guard`  0  THEN  Trivial)

---

Home Index