Proof of Nuprl Lemma : nonce-release-lemma

Step * 1 1 2 1 1 1 2 2 of Lemma nonce-release-lemma

1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. PropertyN
6. ses-ordering'(ses)
7. PropertyF
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. A : Id
16. Honest(A)
17. ∀es:EO+(Info)
      (Honest(A)
      ⇒ (∀e:Act
            ((loc(e) = A ∈ Id)
            ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
               ∧ (∀thr1,thr2:Thread.
                    (e ∈ thr1
                    ⇒ (thr1 is one of bss at A)
                    ⇒ e ∈ thr2
                    ⇒ (thr2 is one of bss at A)
                    ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))
18. es : EO+(Info)
19. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])}
20. (thr is one of bss at A)
21. loc(thr)= A
22. i : ℕ||thr||
23. j : ℕi
24. ↑thr[j] ∈_b New
25. ∀k:{j + 1..i^-}. (¬↑thr[k] ∈_b Send)
26. loc(thr[j]) = A ∈ Id
27. loc(thr[i]) = A ∈ Id
28. e : E@i
29. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* New(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈_b Send)))))
30. Action(e)@i
31. e has* New(thr[j])@i
32. (e <loc thr[i])@i
33. t1 : Thread
34. e ∈ t1
35. (t1 is one of bss at A)
36. loc(t1)= A
37. ∀thr1,thr2:Thread.
      (e ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
38. Legal(t1)@A
39. ¬e ∈ thr
40. ∀e:Act
      (e ∈ t1
      ⇒ e has* New(thr[j])
      ⇒

 (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(thr[j]) ∧ e' ∈ t1)) ∨ (e = thr[j] ∈ E)

supposing ∀e':E. ((e' < e) ⇒ Action(e') ⇒ e' has* New(thr[j]) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈_b Send))))

41. (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(thr[j]) ∧ e' ∈ t1)) ∨ (e = thr[j] ∈ E)

⊢ e ∈ thr
BY
{ D (-1) }

1
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. PropertyN
6. ses-ordering'(ses)
7. PropertyF
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. A : Id
16. Honest(A)
17. ∀es:EO+(Info)
      (Honest(A)
      ⇒ (∀e:Act
            ((loc(e) = A ∈ Id)
            ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
               ∧ (∀thr1,thr2:Thread.
                    (e ∈ thr1
                    ⇒ (thr1 is one of bss at A)
                    ⇒ e ∈ thr2
                    ⇒ (thr2 is one of bss at A)
                    ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))
18. es : EO+(Info)
19. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])}
20. (thr is one of bss at A)
21. loc(thr)= A
22. i : ℕ||thr||
23. j : ℕi
24. ↑thr[j] ∈_b New
25. ∀k:{j + 1..i^-}. (¬↑thr[k] ∈_b Send)
26. loc(thr[j]) = A ∈ Id
27. loc(thr[i]) = A ∈ Id
28. e : E@i
29. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* New(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈_b Send)))))
30. Action(e)@i
31. e has* New(thr[j])@i
32. (e <loc thr[i])@i
33. t1 : Thread
34. e ∈ t1
35. (t1 is one of bss at A)
36. loc(t1)= A
37. ∀thr1,thr2:Thread.
      (e ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
38. Legal(t1)@A
39. ¬e ∈ thr
40. ∀e:Act
      (e ∈ t1
      ⇒ e has* New(thr[j])
      ⇒

 (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(thr[j]) ∧ e' ∈ t1)) ∨ (e = thr[j] ∈ E)

         supposing ∀e':E. ((e' < e) ⇒ Action(e') ⇒ e' has* New(thr[j]) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈_b Send))))
41. ∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(thr[j]) ∧ e' ∈ t1)
⊢ e ∈ thr

2
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. PropertyN
6. ses-ordering'(ses)
7. PropertyF
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. A : Id
16. Honest(A)
17. ∀es:EO+(Info)
      (Honest(A)
      ⇒ (∀e:Act
            ((loc(e) = A ∈ Id)
            ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
               ∧ (∀thr1,thr2:Thread.
                    (e ∈ thr1
                    ⇒ (thr1 is one of bss at A)
                    ⇒ e ∈ thr2
                    ⇒ (thr2 is one of bss at A)
                    ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))
18. es : EO+(Info)
19. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])}
20. (thr is one of bss at A)
21. loc(thr)= A
22. i : ℕ||thr||
23. j : ℕi
24. ↑thr[j] ∈_b New
25. ∀k:{j + 1..i^-}. (¬↑thr[k] ∈_b Send)
26. loc(thr[j]) = A ∈ Id
27. loc(thr[i]) = A ∈ Id
28. e : E@i
29. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* New(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈_b Send)))))
30. Action(e)@i
31. e has* New(thr[j])@i
32. (e <loc thr[i])@i
33. t1 : Thread
34. e ∈ t1
35. (t1 is one of bss at A)
36. loc(t1)= A
37. ∀thr1,thr2:Thread.
      (e ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
38. Legal(t1)@A
39. ¬e ∈ thr
40. ∀e:Act
      (e ∈ t1
      ⇒ e has* New(thr[j])
      ⇒

 (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(thr[j]) ∧ e' ∈ t1)) ∨ (e = thr[j] ∈ E)

supposing ∀e':E. ((e' < e) ⇒ Action(e') ⇒ e' has* New(thr[j]) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈_b Send))))
41. e = thr[j] ∈ E
⊢ e ∈ thr

Latex:

Latex:
1. ses : SES 2. ActionsDisjoint 3. NoncesCiphersAndKeysDisjoint 4. PropertyO 5. PropertyN 6. ses-ordering'(ses) 7. PropertyF 8. PropertyV 9. PropertyR 10. PropertyD 11. PropertyS 12. PropertyK 13. bss : Basic1 List 14. Legal(bss) 15. A : Id 16. Honest(A) 17. \mforall{}es:EO+(Info) (Honest(A) {}\mRightarrow{} (\mforall{}e:Act ((loc(e) = A) {}\mRightarrow{} ((\mexists{}thr:Thread. (e \mmember{} thr \mwedge{} (thr is one of bss at A) \mwedge{} loc(thr)= A)) \mwedge{} (\mforall{}thr1,thr2:Thread. (e \mmember{} thr1 {}\mRightarrow{} (thr1 is one of bss at A) {}\mRightarrow{} e \mmember{} thr2 {}\mRightarrow{} (thr2 is one of bss at A) {}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1))))))) 18. es : EO+(Info) 19. thr : \{thr:Act List| \mforall{}i:\mBbbN{}||thr|| - 1. (thr[i] <loc thr[i + 1])\} 20. (thr is one of bss at A) 21. loc(thr)= A 22. i : \mBbbN{}||thr|| 23. j : \mBbbN{}i 24. \muparrow{}thr[j] \mmember{}\msubb{} New 25. \mforall{}k:\{j + 1..i\msupminus{}\}. (\mneg{}\muparrow{}thr[k] \mmember{}\msubb{} Send) 26. loc(thr[j]) = A 27. loc(thr[i]) = A 28. e : E@i 29. \mforall{}e1:E ((e1 < e) {}\mRightarrow{} Action(e1) {}\mRightarrow{} e1 has* New(thr[j]) {}\mRightarrow{} (((\mneg{}(loc(e1) = A)) {}\mRightarrow{} (thr[i] < e1)) \mwedge{} ((e1 <loc thr[i]) {}\mRightarrow{} (e1 \mmember{} thr \mwedge{} (\mneg{}\muparrow{}e1 \mmember{}\msubb{} Send))))) 30. Action(e)@i 31. e has* New(thr[j])@i 32. (e <loc thr[i])@i 33. t1 : Thread 34. e \mmember{} t1 35. (t1 is one of bss at A) 36. loc(t1)= A 37. \mforall{}thr1,thr2:Thread. (e \mmember{} thr1 {}\mRightarrow{} (thr1 is one of bss at A) {}\mRightarrow{} e \mmember{} thr2 {}\mRightarrow{} (thr2 is one of bss at A) {}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1)) 38. Legal(t1)@A 39. \mneg{}e \mmember{} thr 40. \mforall{}e:Act (e \mmember{} t1 {}\mRightarrow{} e has* New(thr[j]) {}\mRightarrow{} (\mexists{}e':E. ((e' <loc e) \mwedge{} Action(e') \mwedge{} e' has* New(thr[j]) \mwedge{} e' \mmember{} t1)) \mvee{} (e = thr[j]) supposing \mforall{}e':E ((e' < e) {}\mRightarrow{} Action(e') {}\mRightarrow{} e' has* New(thr[j]) {}\mRightarrow{} ((loc(e') = A) \mwedge{} (\mneg{}\muparrow{}e' \mmember{}\msubb{} Send)))) 41. (\mexists{}e':E. ((e' <loc e) \mwedge{} Action(e') \mwedge{} e' has* New(thr[j]) \mwedge{} e' \mmember{} t1)) \mvee{} (e = thr[j]) \mvdash{} e \mmember{} thr By Latex: D (-1) Home Index