---

Step * 4 1 of Lemma ses-act-has-atom


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. ¬↑e ∈b Decrypt
5. ¬↑e ∈b New
6. a : Atom1@i
7. f : E ─→ ℤ
8. False ⇒ (6 = 1 ∈ ℤ)
9. (↑e ∈b Send) ⇒ (6 = 2 ∈ ℤ)
10. (↑e ∈b Rcv) ⇒ (6 = 3 ∈ ℤ)
11. (↑e ∈b Sign) ⇒ (6 = 4 ∈ ℤ)
12. (↑e ∈b Verify) ⇒ (6 = 5 ∈ ℤ)
13. False ⇒ (6 = 7 ∈ ℤ)
14. ↑e ∈b Encrypt
15. (f e) = 6 ∈ ℤ
16. ¬↑e ∈b Rcv
17. ¬↑e ∈b Sign
18. ↑e ∈b Encrypt
19. ¬↑e ∈b Send
20. ¬↑e ∈b Verify
⊢ ¬a#Encrypt(e):SecurityData × Key × Atom1
⇐⇒ (a = cipherText(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e)))
BY
{ (Subst ⌈Encrypt(e) ~ <plainText(e), key(e), cipherText(e)>⌉ 0⋅
   THENL [Complete ((RepUR ``ses-encrypted ses-encryption-key ses-crypt`` 0
                     THEN (GenConclAtAddr [1] THENA Auto)
                     THEN RepeatFor 2 (D -2)
                     THEN Reduce 0
                     THEN Auto))
         ; (((GenConcl ⌈cipherText(e) = b ∈ Atom1⌉⋅ THENA Auto) THEN Thin (-1))
            THEN ((GenConcl ⌈plainText(e) = d ∈ SecurityData⌉⋅ THENA Auto) THEN Thin (-1))
            THEN (GenConcl ⌈key(e) = k ∈ Key⌉⋅ THENA Auto))]
)⋅ }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. ¬↑e ∈b Decrypt
5. ¬↑e ∈b New
6. a : Atom1@i
7. f : E ─→ ℤ
8. False ⇒ (6 = 1 ∈ ℤ)
9. (↑e ∈b Send) ⇒ (6 = 2 ∈ ℤ)
10. (↑e ∈b Rcv) ⇒ (6 = 3 ∈ ℤ)
11. (↑e ∈b Sign) ⇒ (6 = 4 ∈ ℤ)
12. (↑e ∈b Verify) ⇒ (6 = 5 ∈ ℤ)
13. False ⇒ (6 = 7 ∈ ℤ)
14. ↑e ∈b Encrypt
15. (f e) = 6 ∈ ℤ
16. ¬↑e ∈b Rcv
17. ¬↑e ∈b Sign
18. ↑e ∈b Encrypt
19. ¬↑e ∈b Send
20. ¬↑e ∈b Verify
21. b : Atom1@i
22. d : SecurityData@i
23. k : Key@i
24. key(e) = k ∈ Key@i
⊢ ¬a#<d, k, b>:SecurityData × Key × Atom1 ⇐⇒ (a = b ∈ Atom1) ∨ (a ∈ sdata-atoms(d) @ encryption-key-atoms(k))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  Act@i
4.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt
5.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  New
6.  a  :  Atom1@i
7.  f  :  E  {}\mrightarrow{}  \mBbbZ{}
8.  False  {}\mRightarrow{}  (6  =  1)
9.  (\muparrow{}e  \mmember{}\msubb{}  Send)  {}\mRightarrow{}  (6  =  2)
10.  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  (6  =  3)
11.  (\muparrow{}e  \mmember{}\msubb{}  Sign)  {}\mRightarrow{}  (6  =  4)
12.  (\muparrow{}e  \mmember{}\msubb{}  Verify)  {}\mRightarrow{}  (6  =  5)
13.  False  {}\mRightarrow{}  (6  =  7)
14.  \muparrow{}e  \mmember{}\msubb{}  Encrypt
15.  (f  e)  =  6
16.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv
17.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign
18.  \muparrow{}e  \mmember{}\msubb{}  Encrypt
19.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Send
20.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify
\mvdash{}  \mneg{}a\#Encrypt(e):SecurityData  \mtimes{}  Key  \mtimes{}  Atom1
\mLeftarrow{}{}\mRightarrow{}  (a  =  cipherText(e))  \mvee{}  (a  \mmember{}  sdata-atoms(plainText(e))  @  encryption-key-atoms(key(e)))


By

---

Latex:
(Subst  \mkleeneopen{}Encrypt(e)  \msim{}  <plainText(e),  key(e),  cipherText(e)>\mkleeneclose{}  0\mcdot{}
  THENL  [Complete  ((RepUR  ``ses-encrypted  ses-encryption-key  ses-crypt``  0
                                      THEN  (GenConclAtAddr  [1]  THENA  Auto)
                                      THEN  RepeatFor  2  (D  -2)
                                      THEN  Reduce  0
                                      THEN  Auto))
              ;  (((GenConcl  \mkleeneopen{}cipherText(e)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
                    THEN  ((GenConcl  \mkleeneopen{}plainText(e)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
                    THEN  (GenConcl  \mkleeneopen{}key(e)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto))]
)\mcdot{}

---

Home Index