---

Step * 6 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) ⇒ (4 = 1 ∈ ℤ)
7. (↑e ∈b Send) ⇒ (4 = 2 ∈ ℤ)
8. (↑e ∈b Rcv) ⇒ (4 = 3 ∈ ℤ)
9. (↑e ∈b Verify) ⇒ (4 = 5 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ (4 = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (4 = 7 ∈ ℤ)
12. ↑e ∈b Sign
13. (f e) = 4 ∈ ℤ
14. ¬↑e ∈b Rcv
15. ↑e ∈b Sign
16. ¬↑e ∈b Send
⊢ ((↑e ∈b New) ∧ (¬a#New(e):Atom1))
  ∨ ((↑e ∈b Encrypt) ∧ (¬a#Encrypt(e):SecurityData × Key × Atom1))
  ∨ ((↑e ∈b Decrypt) ∧ (¬a#Decrypt(e):SecurityData × Key × Atom1))
  ∨ (¬a#Sign(e):SecurityData × Id × Atom1)
  ∨ ((↑e ∈b Verify) ∧ (¬a#Verify(e):SecurityData × Id × Atom1))
⇐⇒ (a = signature(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(signed(e)))
BY
{ ((BoolCase ⌈e ∈b New⌉⋅ THENA Auto)
   THEN Try ((ThinTrivial THEN (Trivial ORELSE ArithGuard ((MoveToConcl (-1) THEN All Thin THEN Auto))⋅)))
   THEN (BoolCase ⌈e ∈b Decrypt⌉⋅ THENA Auto)
   THEN Try ((ThinTrivial THEN (Trivial ORELSE ArithGuard ((MoveToConcl (-1) THEN All Thin THEN Auto))⋅)))
   THEN (BoolCase ⌈e ∈b Encrypt⌉⋅ THENA Auto)
   THEN Try ((ThinTrivial THEN (Trivial ORELSE ArithGuard ((MoveToConcl (-1) THEN All Thin THEN Auto))⋅)))
   THEN (BoolCase ⌈e ∈b Verify⌉⋅ THENA Auto)
   THEN Try ((ThinTrivial THEN (Trivial ORELSE ArithGuard ((MoveToConcl (-1) THEN All Thin THEN Auto))⋅)))
   THEN (RW (SweepUpC BasicSimpC) 0 THENA Auto))⋅ }

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

---

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{}  (4  =  1)
7.  (\muparrow{}e  \mmember{}\msubb{}  Send)  {}\mRightarrow{}  (4  =  2)
8.  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  (4  =  3)
9.  (\muparrow{}e  \mmember{}\msubb{}  Verify)  {}\mRightarrow{}  (4  =  5)
10.  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  {}\mRightarrow{}  (4  =  6)
11.  (\muparrow{}e  \mmember{}\msubb{}  Decrypt)  {}\mRightarrow{}  (4  =  7)
12.  \muparrow{}e  \mmember{}\msubb{}  Sign
13.  (f  e)  =  4
14.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv
15.  \muparrow{}e  \mmember{}\msubb{}  Sign
16.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Send
\mvdash{}  ((\muparrow{}e  \mmember{}\msubb{}  New)  \mwedge{}  (\mneg{}a\#New(e):Atom1))
    \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (\mneg{}a\#Encrypt(e):SecurityData  \mtimes{}  Key  \mtimes{}  Atom1))
    \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (\mneg{}a\#Decrypt(e):SecurityData  \mtimes{}  Key  \mtimes{}  Atom1))
    \mvee{}  (\mneg{}a\#Sign(e):SecurityData  \mtimes{}  Id  \mtimes{}  Atom1)
    \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Verify)  \mwedge{}  (\mneg{}a\#Verify(e):SecurityData  \mtimes{}  Id  \mtimes{}  Atom1))
\mLeftarrow{}{}\mRightarrow{}  (a  =  signature(e))  \mvee{}  (a  \mmember{}  sdata-atoms(signed(e)))


By

---

Latex:
((BoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  New\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((ThinTrivial
                        THEN  (Trivial  ORELSE  ArithGuard  ((MoveToConcl  (-1)  THEN  All  Thin  THEN  Auto))\mcdot{})
                        ))
  THEN  (BoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  Decrypt\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((ThinTrivial
                        THEN  (Trivial  ORELSE  ArithGuard  ((MoveToConcl  (-1)  THEN  All  Thin  THEN  Auto))\mcdot{})
                        ))
  THEN  (BoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  Encrypt\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((ThinTrivial
                        THEN  (Trivial  ORELSE  ArithGuard  ((MoveToConcl  (-1)  THEN  All  Thin  THEN  Auto))\mcdot{})
                        ))
  THEN  (BoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  Verify\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((ThinTrivial
                        THEN  (Trivial  ORELSE  ArithGuard  ((MoveToConcl  (-1)  THEN  All  Thin  THEN  Auto))\mcdot{})
                        ))
  THEN  (RW  (SweepUpC  BasicSimpC)  0  THENA  Auto))\mcdot{}

---

Home Index