---

Step * of Lemma signature-release-lemma

∀[ses:SES]
  ∀[bss:Basic1 List]
    ∀[A:Id]
      (∀[es:EO+(Info)]. ∀[thr:Thread].
         (∀[i:ℕ||thr||]. ∀[j:ℕi].
            (¬(signature(thr[j]) released before thr[i])) supposing 
               ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
               (↑thr[j] ∈b Sign))) supposing 
            (loc(thr)= A and 
            (thr is one of bss at A))) supposing 
         ((Protocol1(bss) A) and 
         Honest(A)) 
    supposing Legal(bss) ∧ UniqueSignatures(bss) 
  supposing SecurityAxioms
BY
{ (BasicUniformUnivCD ((Auto THEN Auto THEN DoSubsume THEN Auto))⋅
   THEN ((D 0 THENA (DVar `thr' THEN Auto)) THENM Unhide)
   ) }

1
1. ses : SES
2. SecurityAxioms
3. bss : Basic1 List
4. Legal(bss) ∧ UniqueSignatures(bss)
5. A : Id
6. Honest(A)
7. Protocol1(bss) A
8. es : EO+(Info)
9. thr : Thread
10. (thr is one of bss at A)
11. loc(thr)= A
12. i : ℕ||thr||
13. j : ℕi
14. ↑thr[j] ∈b Sign
15. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
16. (signature(thr[j]) released before thr[i])@i
⊢ False

---

Latex:

---

Latex:
\mforall{}[ses:SES]
    \mforall{}[bss:Basic1  List]
        \mforall{}[A:Id]
            (\mforall{}[es:EO+(Info)].  \mforall{}[thr:Thread].
                  (\mforall{}[i:\mBbbN{}||thr||].  \mforall{}[j:\mBbbN{}i].
                        (\mneg{}(signature(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{}  Sign)))  supposing 
                        (loc(thr)=  A  and 
                        (thr  is  one  of  bss  at  A)))  supposing 
                  ((Protocol1(bss)  A)  and 
                  Honest(A)) 
        supposing  Legal(bss)  \mwedge{}  UniqueSignatures(bss) 
    supposing  SecurityAxioms


By

---

Latex:
(BasicUniformUnivCD  ((Auto  THEN  Auto  THEN  DoSubsume  THEN  Auto))\mcdot{}
  THEN  ((D  0  THENA  (DVar  `thr'  THEN  Auto))  THENM  Unhide)
  )

---

Home Index