---

Step * 1 1 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. ∀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))
27. ∀n:E(New). ∀e:E.  ((e has New(n)) ⇒ ses-flow(ses;es;New(n);n;e))
28. ∀e1:E(Sign). ∀b:E.
      ((b has signature(e1))
      ⇒ (∃e2:E(Sign). ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(ses;es;signature(e2);e2;b))))
29. ∃e2:E(Sign). ((Sign(e2) = Sign(thr[j]) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(ses;es;signature(e2);e2;e))
⊢ (thr[i] < e)
BY
{ ExRepD }

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))
27. ∀n:E(New). ∀e:E.  ((e has New(n)) ⇒ ses-flow(ses;es;New(n);n;e))
28. ∀e1:E(Sign). ∀b:E.
      ((b has signature(e1))
      ⇒ (∃e2:E(Sign). ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)) ∧ ses-flow(ses;es;signature(e2);e2;b))))
29. e2 : E(Sign)
30. Sign(e2) = Sign(thr[j]) ∈ (SecurityData × Id × Atom1)
31. ses-flow(ses;es;signature(e2);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.  \mforall{}A:Id
          (Honest(A)
          {}\mRightarrow{}  (Protocol1(bss)  A)
          {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}thr:Thread.
                      ((thr  is  one  of  bss  at  A)
                      {}\mRightarrow{}  (\mforall{}e1,e2:E(Sign).    ((signature(e1)  =  signature(e2))  {}\mRightarrow{}  e1  \mmember{}  thr  {}\mRightarrow{}  (e1  =  e2))))))
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
26.  \mforall{}e2:E(Sign).  ((signature(thr[j])  =  signature(e2))  {}\mRightarrow{}  thr[j]  \mmember{}  thr  {}\mRightarrow{}  (thr[j]  =  e2))
27.  \mforall{}n:E(New).  \mforall{}e:E.    ((e  has  New(n))  {}\mRightarrow{}  ses-flow(ses;es;New(n);n;e))
28.  \mforall{}e1:E(Sign).  \mforall{}b:E.
            ((b  has  signature(e1))
            {}\mRightarrow{}  (\mexists{}e2:E(Sign).  ((Sign(e2)  =  Sign(e1))  \mwedge{}  ses-flow(ses;es;signature(e2);e2;b))))
29.  \mexists{}e2:E(Sign).  ((Sign(e2)  =  Sign(thr[j]))  \mwedge{}  ses-flow(ses;es;signature(e2);e2;e))
\mvdash{}  (thr[i]  <  e)


By

---

Latex:
ExRepD

---

Home Index