---

Step * 1 1 3 1 1 1 1 1 of Lemma cabal-theorem

.....rewrite subgoal..... 
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:Id. ((A@0 ∈ C) ⇒ Honest(A@0))
7. ns : Atom1 List@i
8. ∀a:Atom1
     ((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))))))
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 : E@i
16. y : E@i
17. ∀x1,y1:E.
      (x c≤ x1
      ⇒ x1 c≤ y1
      ⇒ y1 c≤ y
      ⇒ ((x < x1) ∨ (y1 < y))
      ⇒ (∀a:Atom1. (ses-flow(s;es;a;x1;y1) ⇒ y1 c≤ e ⇒ (a ∈ ns) ⇒ (loc(x1) ∈ C) ⇒ (loc(y1) ∈ C))))@i
18. a1 : Atom1@i
19. encr : E(Encrypt)@i
20. decr : E(Decrypt)@i
21. (x <loc encr)@i
22. decr c≤ y@i
23. (encr < decr)@i
24. plainText(decr) = plainText(encr) ∈ SecurityData@i
25. cipherText(decr) = cipherText(encr) ∈ Atom1@i
26. MatchingKeys(key(decr);key(encr))@i
27. ¬(key(decr) = symmetric-key(a1) ∈ Key)@i
28. ses-flow(s;es;a1;x;encr)@i
29. ses-flow(s;es;cipherText(encr);encr;decr)@i
30. ses-flow(s;es;a1;decr;y)@i
31. y c≤ e@i
32. (a1 ∈ ns)@i
33. (loc(x) ∈ C)@i
34. (loc(encr) ∈ C)
35. B : Id
36. (B ∈ C)
37. key(encr) = PublicKey(B) ∈ Key
38. ∀A:Id. (Honest(A) ⇒ (∀e:E(Sign). ((signer(e) = A ∈ Id) ⇒ (loc(e) = A ∈ Id))))
39. ∀A:Id
      (Honest(A)
      ⇒ ((∀e:E(Encrypt). ((key(e) = PrivateKey(A) ∈ Key) ⇒ (loc(e) = A ∈ Id)))
         ∧ (∀e:E(Decrypt). ((key(e) = PrivateKey(A) ∈ Key) ⇒ (loc(e) = A ∈ Id)))))
40. ∀e:E(Encrypt). ((key(e) = PrivateKey(B) ∈ Key) ⇒ (loc(e) = B ∈ Id))
41. ∀e:E(Decrypt). ((key(e) = PrivateKey(B) ∈ Key) ⇒ (loc(e) = B ∈ Id))
⊢ key(decr) = PrivateKey(B) ∈ Key
BY
{ ((Assert PropertyK BY Auto) THEN D (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
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:Id.  ((A@0  \mmember{}  C)  {}\mRightarrow{}  Honest(A@0))
7.  ns  :  Atom1  List@i
8.  \mforall{}a:Atom1
          ((a  \mmember{}  ns)
          {}\mRightarrow{}  ((\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))))))
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.  x  :  E@i
16.  y  :  E@i
17.  \mforall{}x1,y1:E.
            (x  c\mleq{}  x1
            {}\mRightarrow{}  x1  c\mleq{}  y1
            {}\mRightarrow{}  y1  c\mleq{}  y
            {}\mRightarrow{}  ((x  <  x1)  \mvee{}  (y1  <  y))
            {}\mRightarrow{}  (\mforall{}a:Atom1
                        (ses-flow(s;es;a;x1;y1)  {}\mRightarrow{}  y1  c\mleq{}  e  {}\mRightarrow{}  (a  \mmember{}  ns)  {}\mRightarrow{}  (loc(x1)  \mmember{}  C)  {}\mRightarrow{}  (loc(y1)  \mmember{}  C))))@i
18.  a1  :  Atom1@i
19.  encr  :  E(Encrypt)@i
20.  decr  :  E(Decrypt)@i
21.  (x  <loc  encr)@i
22.  decr  c\mleq{}  y@i
23.  (encr  <  decr)@i
24.  plainText(decr)  =  plainText(encr)@i
25.  cipherText(decr)  =  cipherText(encr)@i
26.  MatchingKeys(key(decr);key(encr))@i
27.  \mneg{}(key(decr)  =  symmetric-key(a1))@i
28.  ses-flow(s;es;a1;x;encr)@i
29.  ses-flow(s;es;cipherText(encr);encr;decr)@i
30.  ses-flow(s;es;a1;decr;y)@i
31.  y  c\mleq{}  e@i
32.  (a1  \mmember{}  ns)@i
33.  (loc(x)  \mmember{}  C)@i
34.  (loc(encr)  \mmember{}  C)
35.  B  :  Id
36.  (B  \mmember{}  C)
37.  key(encr)  =  PublicKey(B)
38.  \mforall{}A:Id.  (Honest(A)  {}\mRightarrow{}  (\mforall{}e:E(Sign).  ((signer(e)  =  A)  {}\mRightarrow{}  (loc(e)  =  A))))
39.  \mforall{}A:Id
            (Honest(A)
            {}\mRightarrow{}  ((\mforall{}e:E(Encrypt).  ((key(e)  =  PrivateKey(A))  {}\mRightarrow{}  (loc(e)  =  A)))
                  \mwedge{}  (\mforall{}e:E(Decrypt).  ((key(e)  =  PrivateKey(A))  {}\mRightarrow{}  (loc(e)  =  A)))))
40.  \mforall{}e:E(Encrypt).  ((key(e)  =  PrivateKey(B))  {}\mRightarrow{}  (loc(e)  =  B))
41.  \mforall{}e:E(Decrypt).  ((key(e)  =  PrivateKey(B))  {}\mRightarrow{}  (loc(e)  =  B))
\mvdash{}  key(decr)  =  PrivateKey(B)


By

---

Latex:
((Assert  PropertyK  BY  Auto)  THEN  D  (-1)  THEN  Auto)\mcdot{}

---

Home Index