---

Step * of Lemma ses-flow-implies

∀s:SES. ∀es:EO+(Info).
  ∀[P:E ─→ E ─→ Atom1 ─→ ℙ]
    ((∀e1,e2:E. ∀a:Atom1.  (((e1 has a) ∧ (e2 has a) ∧ e1 ≤loc e2 ) ⇒ P[e1;e2;a]))
    ⇒ (∀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] ∧ P[rcv;e2;a])
          ⇒ P[e1;e2;a]))
    ⇒ (∀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]
          ∧ P[encr;decr;cipherText(encr)]
          ∧ P[decr;e2;a])
          ⇒ P[e1;e2;a]))
    ⇒ {∀e1,e2:E. ∀a:Atom1.  (ses-flow(s;es;a;e1;e2) ⇒ P[e1;e2;a])})
BY
{ (InstLemma `ses-flow-implies\'` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN (D (-3) THENA (ParallelOp (-2) THEN RepeatFor 5 ((ParallelLast THENA Auto))))
   THEN (D (-1) THENA (ParallelOp (-1) THEN RepeatFor 5 ((ParallelLast THENA Auto)))⋅)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).
    \mforall{}[P:E  {}\mrightarrow{}  E  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}e1,e2:E.  \mforall{}a:Atom1.    (((e1  has  a)  \mwedge{}  (e2  has  a)  \mwedge{}  e1  \mleq{}loc  e2  )  {}\mRightarrow{}  P[e1;e2;a]))
        {}\mRightarrow{}  (\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{}  P[rcv;e2;a])
                    {}\mRightarrow{}  P[e1;e2;a]))
        {}\mRightarrow{}  (\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{}  P[encr;decr;cipherText(encr)]
                    \mwedge{}  P[decr;e2;a])
                    {}\mRightarrow{}  P[e1;e2;a]))
        {}\mRightarrow{}  \{\mforall{}e1,e2:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;e1;e2)  {}\mRightarrow{}  P[e1;e2;a])\})


By

---

Latex:
(InstLemma  `ses-flow-implies\mbackslash{}'`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  (D  (-3)  THENA  (ParallelOp  (-2)  THEN  RepeatFor  5  ((ParallelLast  THENA  Auto))))
  THEN  (D  (-1)  THENA  (ParallelOp  (-1)  THEN  RepeatFor  5  ((ParallelLast  THENA  Auto)))\mcdot{})
  THEN  Trivial)

---

Home Index