---

Step * 7 of Lemma ses-act-has-atom


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ─→ ℤ
6. (↑e ∈b New) ⇒ (5 = 1 ∈ ℤ)
7. (↑e ∈b Send) ⇒ (5 = 2 ∈ ℤ)
8. (↑e ∈b Rcv) ⇒ (5 = 3 ∈ ℤ)
9. (↑e ∈b Sign) ⇒ (5 = 4 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ (5 = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (5 = 7 ∈ ℤ)
12. ↑e ∈b Verify
13. (f e) = 5 ∈ ℤ
14. ¬↑e ∈b Rcv
15. ¬↑e ∈b Sign
16. ¬↑e ∈b Encrypt
17. ¬↑e ∈b Decrypt
18. ¬↑e ∈b New
19. ¬↑e ∈b Send
20. ↑e ∈b Verify
⊢ ¬a#Verify(e):SecurityData × Id × Atom1 ⇐⇒ (a ∈ [signature(e) / sdata-atoms(signed(e))])
BY
{ (Subst ⌈Verify(e) ~ <signed(e), signer(e), signature(e)>⌉ 0⋅
   THENL [Complete ((RepUR ``ses-verify-signed ses-verify-signer ses-verify-sig`` 0
                     THEN (GenConclAtAddr [1] THENA Auto)
                     THEN RepeatFor 2 (D -2)
                     THEN Reduce 0
                     THEN Auto))
         ; (((GenConcl ⌈signature(e) = b ∈ Atom1⌉⋅ THENA Auto) THEN Thin (-1))
            THEN ((GenConcl ⌈signed(e) = d ∈ SecurityData⌉⋅ THENA Auto) THEN Thin (-1))
            THEN (GenConcl ⌈signer(e) = k ∈ Id⌉⋅ THENA Auto)
            THEN All Thin
            THEN ((RWO "free-from-atom-pair-iff" 0 THENA Auto)⋅
                  THEN (Assert a#<k, b>:Id × Atom1 ∈ Type BY
                              Auto)
                  THEN (RWO  "sdata-free-from-atom" 0 THENA Auto)
                  THEN (RWO "free-from-atom-pair-iff" 0 THENA Auto)
                  THEN (Assert a#k:Id ∈ Type BY
                              Auto)
                  THEN (RWO "free-from-atom-atom" 0 THENA Auto)
                  THEN (RWO "free-from-atom-Id-rw" 0 THENA Auto)⋅)⋅)]
)⋅ }

1
1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Id@i
5. a#<k, b>:Id × Atom1 ∈ Type
6. a#k:Id ∈ Type
⊢ ¬((¬(a ∈ sdata-atoms(d))) ∧ True ∧ (¬(b = a ∈ Atom1))) ⇐⇒ (a ∈ [b / sdata-atoms(d)])

---

Latex:

---

Latex:

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


By

---

Latex:
(Subst  \mkleeneopen{}Verify(e)  \msim{}  <signed(e),  signer(e),  signature(e)>\mkleeneclose{}  0\mcdot{}
  THENL  [Complete  ((RepUR  ``ses-verify-signed  ses-verify-signer  ses-verify-sig``  0
                                      THEN  (GenConclAtAddr  [1]  THENA  Auto)
                                      THEN  RepeatFor  2  (D  -2)
                                      THEN  Reduce  0
                                      THEN  Auto))
              ;  (((GenConcl  \mkleeneopen{}signature(e)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
                    THEN  ((GenConcl  \mkleeneopen{}signed(e)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
                    THEN  (GenConcl  \mkleeneopen{}signer(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>:Id  \mtimes{}  Atom1  \mmember{}  Type  BY
                                                        Auto)
                                THEN  (RWO    "sdata-free-from-atom"  0  THENA  Auto)
                                THEN  (RWO  "free-from-atom-pair-iff"  0  THENA  Auto)
                                THEN  (Assert  a\#k:Id  \mmember{}  Type  BY
                                                        Auto)
                                THEN  (RWO  "free-from-atom-atom"  0  THENA  Auto)
                                THEN  (RWO  "free-from-atom-Id-rw"  0  THENA  Auto)\mcdot{})\mcdot{})]
)\mcdot{}

---

Home Index