---

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


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. ¬↑e ∈b New
5. a : Atom1@i
6. f : E ─→ ℤ
7. False ⇒ (7 = 1 ∈ ℤ)
8. (↑e ∈b Send) ⇒ (7 = 2 ∈ ℤ)
9. (↑e ∈b Rcv) ⇒ (7 = 3 ∈ ℤ)
10. (↑e ∈b Sign) ⇒ (7 = 4 ∈ ℤ)
11. (↑e ∈b Verify) ⇒ (7 = 5 ∈ ℤ)
12. (↑e ∈b Encrypt) ⇒ (7 = 6 ∈ ℤ)
13. ↑e ∈b Decrypt
14. (f e) = 7 ∈ ℤ
15. ¬↑e ∈b Rcv
16. ¬↑e ∈b Sign
17. ¬↑e ∈b Encrypt
18. ↑e ∈b Decrypt
19. ¬↑e ∈b Send
20. ¬↑e ∈b Verify
⊢ ¬a#Decrypt(e):SecurityData × Key × Atom1
⇐⇒ (a ∈ sdata-atoms(plainText(e))) ∨ (a ∈ [cipherText(e) / encryption-key-atoms(key(e))])
BY
{ (Subst ⌈Decrypt(e) ~ <plainText(e), key(e), cipherText(e)>⌉ 0⋅
   THENL [Complete ((RepUR ``ses-decrypted ses-decryption-key ses-cipher`` 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)
            THEN All Thin
            THEN (RWO "free-from-atom-pair-iff" 0 THENA Auto)⋅
            THEN (Assert a#<k, b>:Key × Atom1 ∈ Type BY
                        Auto)
            THEN (Assert a#b:Atom1 ∈ Type BY
                        Auto)
            THEN (Assert a#d:SecurityData ∈ Type BY
                        Auto))]
)⋅ }

1
1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Key@i
5. a#<k, b>:Key × Atom1 ∈ Type
6. a#b:Atom1 ∈ Type
7. a#d:SecurityData ∈ Type
⊢ ¬(a#d:SecurityData ∧ a#<k, b>:Key × Atom1) ⇐⇒ (a ∈ sdata-atoms(d)) ∨ (a ∈ [b / 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{}  New
5.  a  :  Atom1@i
6.  f  :  E  {}\mrightarrow{}  \mBbbZ{}
7.  False  {}\mRightarrow{}  (7  =  1)
8.  (\muparrow{}e  \mmember{}\msubb{}  Send)  {}\mRightarrow{}  (7  =  2)
9.  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  (7  =  3)
10.  (\muparrow{}e  \mmember{}\msubb{}  Sign)  {}\mRightarrow{}  (7  =  4)
11.  (\muparrow{}e  \mmember{}\msubb{}  Verify)  {}\mRightarrow{}  (7  =  5)
12.  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  {}\mRightarrow{}  (7  =  6)
13.  \muparrow{}e  \mmember{}\msubb{}  Decrypt
14.  (f  e)  =  7
15.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv
16.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign
17.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt
18.  \muparrow{}e  \mmember{}\msubb{}  Decrypt
19.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Send
20.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify
\mvdash{}  \mneg{}a\#Decrypt(e):SecurityData  \mtimes{}  Key  \mtimes{}  Atom1
\mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  sdata-atoms(plainText(e)))  \mvee{}  (a  \mmember{}  [cipherText(e)  /  encryption-key-atoms(key(e))])


By

---

Latex:
(Subst  \mkleeneopen{}Decrypt(e)  \msim{}  <plainText(e),  key(e),  cipherText(e)>\mkleeneclose{}  0\mcdot{}
  THENL  [Complete  ((RepUR  ``ses-decrypted  ses-decryption-key  ses-cipher``  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)
                    THEN  All  Thin
                    THEN  (RWO  "free-from-atom-pair-iff"  0  THENA  Auto)\mcdot{}
                    THEN  (Assert  a\#<k,  b>:Key  \mtimes{}  Atom1  \mmember{}  Type  BY
                                            Auto)
                    THEN  (Assert  a\#b:Atom1  \mmember{}  Type  BY
                                            Auto)
                    THEN  (Assert  a\#d:SecurityData  \mmember{}  Type  BY
                                            Auto))]
)\mcdot{}

---

Home Index