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