Proof of Nuprl Lemma : cabal-theorem

Step * 1 2 2 of Lemma cabal-theorem

1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
((loc(e) = i ∈ Id)
∧ (((↑e ∈_b New) ∧ (a = New(e) ∈ Atom1))

                    ∨ ((↑e ∈_b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))

                 ((Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)) ∧ ses-flow(s;es;cipherText(e2);e2;e)) BY

               Auto)
   THEN ExRepD
   THEN Assert ⌈(loc(e2) ∈ C)⌉⋅)⋅ }

1
.....assertion.....
1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
                  ((loc(e) = i ∈ Id)
                  ∧ (((↑e ∈_b New) ∧ (a = New(e) ∈ Atom1))

                    ∨ ((↑e ∈_b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))

      ∧ (∀e:E(Send). ((loc(e) ∈ C) ⇒ (¬(e has a))))
      ∧ (∀e:E(Encrypt)
           ((loc(e) ∈ C)
           ⇒ (e has a)
           ⇒ ((∃A∈C. key(e) = PublicKey(A) ∈ Key)
              ∨ (∃k∈ns. key(e) = symmetric-key(k) ∈ Key)
              ∨ (cipherText(e) ∈ ns)))))@i
9. PropertyF
10. e : E@i
11. ∀e1:E. ((e1 < e) ⇒ (∃a∈ns. (e1 has a)) ⇒ (loc(e1) ∈ C))
12. a : Atom1
13. (a ∈ ns)
14. (e has a)
15. ∀x,y:E. ∀a:Atom1.  (ses-flow(s;es;a;x;y) ⇒ y c≤ e ⇒ (a ∈ ns) ⇒ (loc(x) ∈ C) ⇒ (loc(y) ∈ C))
16. i : Id
17. (i ∈ C)
18. encr : E
19. loc(encr) = i ∈ Id
20. ↑encr ∈_b Encrypt
21. a = cipherText(encr) ∈ Atom1
22. (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (encr has b))
23. e2 : E(Encrypt)
24. Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)
25. ses-flow(s;es;cipherText(e2);e2;e)
⊢ (loc(e2) ∈ C)

2
1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
                  ((loc(e) = i ∈ Id)
                  ∧ (((↑e ∈_b New) ∧ (a = New(e) ∈ Atom1))

                    ∨ ((↑e ∈_b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))

Latex:

Latex:
1. s : SES@i' 2. A : SecurityAxioms@i' 3. s2 : Top@i' 4. es : EO+(Info)@i' 5. C : Id List@i 6. (\mforall{}A@0\mmember{}C.Honest(A@0)) 7. ns : Atom1 List@i 8. (\mforall{}a\mmember{}ns.(\mexists{}i\mmember{}C. \mexists{}e:E ((loc(e) = i) \mwedge{} (((\muparrow{}e \mmember{}\msubb{} New) \mwedge{} (a = New(e))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Encrypt) \mwedge{} (a = cipherText(e)) \mwedge{} (\mexists{}b\mmember{}ns. (\mneg{}(b = a)) \mwedge{} (e has b)))))) \mwedge{} (\mforall{}e:E(Send). ((loc(e) \mmember{} C) {}\mRightarrow{} (\mneg{}(e has a)))) \mwedge{} (\mforall{}e:E(Encrypt) ((loc(e) \mmember{} C) {}\mRightarrow{} (e has a) {}\mRightarrow{} ((\mexists{}A\mmember{}C. key(e) = PublicKey(A)) \mvee{} (\mexists{}k\mmember{}ns. key(e) = symmetric-key(k)) \mvee{} (cipherText(e) \mmember{} ns)))))@i 9. PropertyF 10. e : E@i 11. \mforall{}e1:E. ((e1 < e) {}\mRightarrow{} (\mexists{}a\mmember{}ns. (e1 has a)) {}\mRightarrow{} (loc(e1) \mmember{} C)) 12. a : Atom1 13. (a \mmember{} ns) 14. (e has a) 15. \mforall{}x,y:E. \mforall{}a:Atom1. (ses-flow(s;es;a;x;y) {}\mRightarrow{} y c\mleq{} e {}\mRightarrow{} (a \mmember{} ns) {}\mRightarrow{} (loc(x) \mmember{} C) {}\mRightarrow{} (loc(y) \mmember{} C)) 16. i : Id 17. (i \mmember{} C) 18. e1 : E 19. loc(e1) = i 20. \muparrow{}e1 \mmember{}\msubb{} Encrypt 21. a = cipherText(e1) 22. (\mexists{}b\mmember{}ns. (\mneg{}(b = a)) \mwedge{} (e1 has b)) \mvdash{} (loc(e) \mmember{} C) By Latex: (RenameVar `encr' (-5) THEN (Assert \mexists{}e2:E(Encrypt) ((Encrypt(e2) = Encrypt(encr)) \mwedge{} ses-flow(s;es;cipherText(e2);e2;e)) BY Auto) THEN ExRepD THEN Assert \mkleeneopen{}(loc(e2) \mmember{} C)\mkleeneclose{}\mcdot{})\mcdot{} Home Index