---

Step * of Lemma ses-legal-thread-decrypt

∀s:SES
  (ActionsDisjoint
  ⇒ PropertyD
     ⇒ (∀es:EO+(Info). ∀A:Id. ∀thr:Thread. ∀e:E.
           (Legal(thr)@A
           ⇒ e ∈ thr ⇒ (∃a:Act. ((a <loc e) ∧ a ∈ thr ∧ (a has cipherText(e)))) supposing ↑e ∈b Decrypt)) 
     supposing NoncesCiphersAndKeysDisjoint)
BY
{ (RepUR ``ses-thread-member ses-thread ses-legal-thread`` 0 THEN Auto THEN ExRepD) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. NoncesCiphersAndKeysDisjoint
4. PropertyD@i'
5. es : EO+(Info)@i'
6. A : Id@i
7. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
8. e : E@i
9. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
10. ↑e ∈b Decrypt
11. i : ℕ||thr||@i
12. e = thr[i] ∈ E@i
⊢ ∃a:Act. ((a <loc e) ∧ (∃i:ℕ||thr||. (a = thr[i] ∈ E)) ∧ (a has cipherText(e)))

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  PropertyD
          {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}A:Id.  \mforall{}thr:Thread.  \mforall{}e:E.
                      (Legal(thr)@A
                      {}\mRightarrow{}  e  \mmember{}  thr  {}\mRightarrow{}  (\mexists{}a:Act.  ((a  <loc  e)  \mwedge{}  a  \mmember{}  thr  \mwedge{}  (a  has  cipherText(e)))) 
                            supposing  \muparrow{}e  \mmember{}\msubb{}  Decrypt)) 
          supposing  NoncesCiphersAndKeysDisjoint)


By

---

Latex:
(RepUR  ``ses-thread-member  ses-thread  ses-legal-thread``  0  THEN  Auto  THEN  ExRepD)

---

Home Index