---

Step * of Lemma member-used-atoms

∀s:SES
  (ActionsDisjoint
  ⇒ (∀es:EO+(Info). ∀e:E. ∀a:Atom1.
        ((a ∈ UsedAtoms(e))
        ⇐⇒ ((↑e ∈b Send) ∧ (a ∈ sdata-atoms(Send(e))))
            ∨ ((↑e ∈b Decrypt) ∧ ((a = cipherText(e) ∈ Atom1) ∨ (a ∈ encryption-key-atoms(key(e)))))
            ∨ ((↑e ∈b Verify) ∧ ((a = signature(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(signed(e)))))
            ∨ ((↑e ∈b Sign) ∧ (a ∈ sdata-atoms(signed(e))))
            ∨ ((↑e ∈b Encrypt) ∧ ((a ∈ sdata-atoms(plainText(e))) ∨ (a ∈ encryption-key-atoms(key(e))))))))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN Unfold `ses-used-atoms` 0
   THEN Unfold `ses-disjoint` 2
   THEN ((InstHyp [⌜es⌝] 2⋅ THENM Thin 2) THENA Auto)
   THEN (D -1 THEN (InstHyp [⌜e⌝] (-1)⋅ THENA Auto) THEN Thin (-2))
   THEN SplitAndHyps
   THEN Repeat ((WeakAutoSplit THEN ThinTrivial THEN Try (Arith)))
   THEN ((RepeatFor 2 (D 0) THENA Auto) THEN SplitOrHyps THEN SplitAndHyps THEN ThinTrivial THEN Try (Arith) THEN Auto)
   ⋅) }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ¬↑e ∈b Sign
5. ¬↑e ∈b Send
6. a : Atom1@i
7. f : E ⟶ ℤ
8. (↑e ∈b New) ⇒ ((f e) = 1 ∈ ℤ)
9. (↑e ∈b Rcv) ⇒ ((f e) = 3 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ ((f e) = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ ((f e) = 7 ∈ ℤ)
12. ↑e ∈b Verify
13. (f e) = 5 ∈ ℤ
14. (a ∈ [signature(e) / sdata-atoms(signed(e))])@i
⊢ ((↑e ∈b Decrypt) ∧ ((a = cipherText(e) ∈ Atom1) ∨ (a ∈ encryption-key-atoms(key(e)))))
∨ (True ∧ ((a = signature(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(signed(e)))))
∨ (False ∧ (a ∈ sdata-atoms(signed(e))))
∨ ((↑e ∈b Encrypt) ∧ ((a ∈ sdata-atoms(plainText(e))) ∨ (a ∈ encryption-key-atoms(key(e)))))

2
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ¬↑e ∈b Verify
5. ¬↑e ∈b Sign
6. ¬↑e ∈b Send
7. a : Atom1@i
8. f : E ⟶ ℤ
9. (↑e ∈b New) ⇒ ((f e) = 1 ∈ ℤ)
10. (↑e ∈b Rcv) ⇒ ((f e) = 3 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ ((f e) = 7 ∈ ℤ)
12. ↑e ∈b Encrypt
13. (f e) = 6 ∈ ℤ
14. (a ∈ sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e)))@i
⊢ ((↑e ∈b Decrypt) ∧ ((a = cipherText(e) ∈ Atom1) ∨ (a ∈ encryption-key-atoms(key(e)))))
∨ (False ∧ ((a = signature(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(signed(e)))))
∨ (False ∧ (a ∈ sdata-atoms(signed(e))))
∨ (True ∧ ((a ∈ sdata-atoms(plainText(e))) ∨ (a ∈ encryption-key-atoms(key(e)))))

3
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ¬↑e ∈b Encrypt
5. ¬↑e ∈b Verify
6. ¬↑e ∈b Sign
7. ¬↑e ∈b Send
8. a : Atom1@i
9. f : E ⟶ ℤ
10. (↑e ∈b New) ⇒ ((f e) = 1 ∈ ℤ)
11. (↑e ∈b Rcv) ⇒ ((f e) = 3 ∈ ℤ)
12. ↑e ∈b Decrypt
13. (f e) = 7 ∈ ℤ
14. (a ∈ [cipherText(e) / encryption-key-atoms(key(e))])@i
15. True
⊢ (a = cipherText(e) ∈ Atom1) ∨ (a ∈ encryption-key-atoms(key(e)))

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}a:Atom1.
                ((a  \mmember{}  UsedAtoms(e))
                \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (a  \mmember{}  sdata-atoms(Send(e))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Decrypt)  \mwedge{}  ((a  =  cipherText(e))  \mvee{}  (a  \mmember{}  encryption-key-atoms(key(e)))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Verify)  \mwedge{}  ((a  =  signature(e))  \mvee{}  (a  \mmember{}  sdata-atoms(signed(e)))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  (a  \mmember{}  sdata-atoms(signed(e))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)
                            \mwedge{}  ((a  \mmember{}  sdata-atoms(plainText(e)))  \mvee{}  (a  \mmember{}  encryption-key-atoms(key(e))))))))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  Unfold  `ses-used-atoms`  0
  THEN  Unfold  `ses-disjoint`  2
  THEN  ((InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  2\mcdot{}  THENM  Thin  2)  THENA  Auto)
  THEN  (D  -1  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Thin  (-2))
  THEN  SplitAndHyps
  THEN  Repeat  ((WeakAutoSplit  THEN  ThinTrivial  THEN  Try  (Arith)))
  THEN  ((RepeatFor  2  (D  0)  THENA  Auto)
              THEN  SplitOrHyps
              THEN  SplitAndHyps
              THEN  ThinTrivial
              THEN  Try  (Arith)
              THEN  Auto)\mcdot{})

---

Home Index