---

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] ∧ ses-flow(s;es;a;e1;snd))
          ∧ P[rcv;e2;a]
          ∧ ses-flow(s;es;a;rcv;e2))
          ⇒ 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] ∧ 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]))
    ⇒ {∀e1,e2:E. ∀a:Atom1.  (ses-flow(s;es;a;e1;e2) ⇒ P[e1;e2;a])})
BY
{ (Auto⋅ THEN Auto THEN (InstLemma `ses-flow-induction` [⌜s⌝;⌜es⌝;⌜P⌝]⋅ THENA Auto)) }

1
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. ses-flow(s;es;a;e1;e2)@i
⊢ P[e1;e2;a]

2
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])}

---

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


By

---

Latex:
(Auto\mcdot{}  THEN  Auto  THEN  (InstLemma  `ses-flow-induction`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index