Step
*
of Lemma
nonce-release-lemma2
∀[s:SecurityTheory]. ∀[bss:Basic1 List].
∀[A:Id]
(∀[es:EO+(Info)]. ∀[thr:Thread].
(∀[i:ℕ||thr||]. ∀[j:ℕi].
(¬(New(thr[j]) released before thr[i])) supposing
((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and
(↑thr[j] ∈b New))) supposing
(loc(thr)= A and
(thr is one of bss at A))) supposing
((Protocol1(bss) A) and
Honest(A))
supposing Legal(bss)
BY
{ Auto }
1
1. s : SecurityTheory
2. bss : Basic1 List
3. Legal(bss)
4. A : Id
5. Honest(A)
6. Protocol1(bss) A
7. es : EO+(Info)
8. thr : Thread
9. (thr is one of bss at A)
10. loc(thr)= A
11. i : ℕ||thr||
12. j : ℕi
13. ↑thr[j] ∈b New
14. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
⊢ ¬(New(thr[j]) released before thr[i])
Latex:
Latex:
\mforall{}[s:SecurityTheory]. \mforall{}[bss:Basic1 List].
\mforall{}[A:Id]
(\mforall{}[es:EO+(Info)]. \mforall{}[thr:Thread].
(\mforall{}[i:\mBbbN{}||thr||]. \mforall{}[j:\mBbbN{}i].
(\mneg{}(New(thr[j]) released before thr[i])) supposing
((\mforall{}k:\{j + 1..i\msupminus{}\}. (\mneg{}\muparrow{}thr[k] \mmember{}\msubb{} Send)) and
(\muparrow{}thr[j] \mmember{}\msubb{} New))) supposing
(loc(thr)= A and
(thr is one of bss at A))) supposing
((Protocol1(bss) A) and
Honest(A))
supposing Legal(bss)
By
Latex:
Auto
Home
Index