---

Step * 1 of Lemma nonce-release-lemma2


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])
BY
{ (D 1
   THEN D 2
   THEN All (RepUR ``sth-es`` )⋅
   THEN ((InstLemma `nonce-release-lemma` [⌈ses⌉;⌈bss⌉;⌈A⌉]⋅ THENM BHyp -1 ) THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

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  :  \mBbbN{}||thr||
12.  j  :  \mBbbN{}i
13.  \muparrow{}thr[j]  \mmember{}\msubb{}  New
14.  \mforall{}k:\{j  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}thr[k]  \mmember{}\msubb{}  Send)
\mvdash{}  \mneg{}(New(thr[j])  released  before  thr[i])


By

---

Latex:
(D  1
  THEN  D  2
  THEN  All  (RepUR  ``sth-es``  )\mcdot{}
  THEN  ((InstLemma  `nonce-release-lemma`  [\mkleeneopen{}ses\mkleeneclose{};\mkleeneopen{}bss\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENM  BHyp  -1  )  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index