---

Step * 1 of Lemma signature-release-lemma2


1. ses : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. ∀[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)
5. bss : Basic1 List@i'
6. Legal(bss)@i'
7. FreshSignatures(bss)@i'
8. UniqueSignatures(bss)
9. A@0 : Id@i
10. Honest(A@0)
11. Protocol1(bss) A@0@i'
12. es : EO+(Info)@i'
13. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr is one of bss at A@0)@i'
15. loc(thr)= A@0
16. ∀[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))
17. i : ℕ||thr||@i
18. ∀[j:ℕi]
      (¬(signature(thr[j]) released before thr[i])) supposing 
         ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
         (↑thr[j] ∈b Sign))
19. j : ℕi@i
20. ↑thr[j] ∈b Sign@i
21. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)@i
22. ¬(signature(thr[j]) released before thr[i])
23. e : E@i
24. ¬(loc(e) = A@0 ∈ Id)@i
25. (e has signature(thr[j]))@i
⊢ (thr[i] < e)
BY
{ (RepUR ``unique-sig-protocol noncelike-signatures`` 8 THEN (InstHyp [⌈A@0⌉;⌈es⌉;⌈thr⌉;⌈thr[j]⌉] 8⋅ THENA Auto)) }

1
1. ses : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. ∀[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)
5. bss : Basic1 List@i'
6. Legal(bss)@i'
7. FreshSignatures(bss)@i'
8. ∀A:Id
     (Honest(A)
     ⇒ (Protocol1(bss) A)
     ⇒ (∀es:EO+(Info). ∀thr:Thread.
           ((thr is one of bss at A)
           ⇒ (∀e1,e2:E(Sign).  ((signature(e1) = signature(e2) ∈ Atom1) ⇒ e1 ∈ thr ⇒ (e1 = e2 ∈ E))))))
9. A@0 : Id@i
10. Honest(A@0)
11. Protocol1(bss) A@0@i'
12. es : EO+(Info)@i'
13. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr is one of bss at A@0)@i'
15. loc(thr)= A@0
16. ∀[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))
17. i : ℕ||thr||@i
18. ∀[j:ℕi]
      (¬(signature(thr[j]) released before thr[i])) supposing 
         ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
         (↑thr[j] ∈b Sign))
19. j : ℕi@i
20. ↑thr[j] ∈b Sign@i
21. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)@i
22. ¬(signature(thr[j]) released before thr[i])
23. e : E@i
24. ¬(loc(e) = A@0 ∈ Id)@i
25. (e has signature(thr[j]))@i
26. ∀e2:E(Sign). ((signature(thr[j]) = signature(e2) ∈ Atom1) ⇒ thr[j] ∈ thr ⇒ (thr[j] = e2 ∈ E))
⊢ (thr[i] < e)

---

Latex:

---

Latex:

1.  ses  :  SES@i'
2.  A  :  SecurityAxioms@i'
3.  s2  :  Top@i'
4.  \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)
5.  bss  :  Basic1  List@i'
6.  Legal(bss)@i'
7.  FreshSignatures(bss)@i'
8.  UniqueSignatures(bss)
9.  A@0  :  Id@i
10.  Honest(A@0)
11.  Protocol1(bss)  A@0@i'
12.  es  :  EO+(Info)@i'
13.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\}  @i
14.  (thr  is  one  of  bss  at  A@0)@i'
15.  loc(thr)=  A@0
16.  \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))
17.  i  :  \mBbbN{}||thr||@i
18.  \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))
19.  j  :  \mBbbN{}i@i
20.  \muparrow{}thr[j]  \mmember{}\msubb{}  Sign@i
21.  \mforall{}k:\{j  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}thr[k]  \mmember{}\msubb{}  Send)@i
22.  \mneg{}(signature(thr[j])  released  before  thr[i])
23.  e  :  E@i
24.  \mneg{}(loc(e)  =  A@0)@i
25.  (e  has  signature(thr[j]))@i
\mvdash{}  (thr[i]  <  e)


By

---

Latex:
(RepUR  ``unique-sig-protocol  noncelike-signatures``  8
  THEN  (InstHyp  [\mkleeneopen{}A@0\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}thr\mkleeneclose{};\mkleeneopen{}thr[j]\mkleeneclose{}]  8\mcdot{}  THENA  Auto)
  )

---

Home Index