---

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