Step
*
of Lemma
ses-act-has-atom
∀s:SES
(ActionsDisjoint ⇒ (∀es:EO+(Info). ∀e:Act. ∀a:Atom1. ((e has a) ⇐⇒ (a ∈ UseableAtoms(e)) ∨ (a ∈ UsedAtoms(e)))))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
THEN RepUR ``event-has class-value-has ses-useable-atoms ses-used-atoms`` 0
THEN Unfold `ses-disjoint` 2
THEN ((InstHyp [⌜es⌝] 2⋅ THENM (Thin 2 THEN D -1)) THENA Auto)
THEN ((InstHyp [⌜e⌝] (-1)⋅ THENM Thin (-2)) THENA Auto)
THEN (Assert Action(e) BY
(DVar `e' THEN Unhide THEN Auto))
THEN SplitAndHyps
THEN Unfold `ses-action` -1
THEN SplitOrHyps
THEN ThinTrivial
THEN SplitAndHyps
THEN ThinTrivial
THEN Eliminate ⌜f e⌝⋅
THEN Repeat (UnitProgress(((SplitOnConclITE THENA Auto)
THEN Try ((ThinTrivial
THEN (Trivial ORELSE ArithGuard ((MoveToConcl (-1) THEN All Thin THEN Auto))⋅)
))
))⋅)
THEN Reduce 0
THEN (RWW "nil_member member_singleton" 0 THENA Auto)
THEN (RW (SweepUpC BasicSimpC) 0 THENA Auto)) }
1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ⟶ ℤ
6. (↑e ∈b Send) ⇒ (1 = 2 ∈ ℤ)
7. (↑e ∈b Rcv) ⇒ (1 = 3 ∈ ℤ)
8. (↑e ∈b Sign) ⇒ (1 = 4 ∈ ℤ)
9. (↑e ∈b Verify) ⇒ (1 = 5 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ (1 = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (1 = 7 ∈ ℤ)
12. ↑e ∈b New
13. (f e) = 1 ∈ ℤ
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#New(e):Atom1 ⇐⇒ a = New(e) ∈ Atom1
2
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ⟶ ℤ
6. (↑e ∈b New) ⇒ (2 = 1 ∈ ℤ)
7. (↑e ∈b Rcv) ⇒ (2 = 3 ∈ ℤ)
8. (↑e ∈b Sign) ⇒ (2 = 4 ∈ ℤ)
9. (↑e ∈b Verify) ⇒ (2 = 5 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ (2 = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (2 = 7 ∈ ℤ)
12. ↑e ∈b Send
13. (f e) = 2 ∈ ℤ
14. ¬↑e ∈b Rcv
15. ¬↑e ∈b Sign
16. ¬↑e ∈b Encrypt
17. ¬↑e ∈b Decrypt
18. ¬↑e ∈b New
19. ↑e ∈b Send
⊢ (¬a#Send(e):SecurityData) ∨ ((↑e ∈b Verify) ∧ (¬a#Verify(e):SecurityData × Id × Atom1)) ⇐⇒ (a ∈ sdata-atoms(Send(e)))
3
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ⟶ ℤ
6. (↑e ∈b New) ⇒ (3 = 1 ∈ ℤ)
7. (↑e ∈b Send) ⇒ (3 = 2 ∈ ℤ)
8. (↑e ∈b Sign) ⇒ (3 = 4 ∈ ℤ)
9. (↑e ∈b Verify) ⇒ (3 = 5 ∈ ℤ)
10. (↑e ∈b Encrypt) ⇒ (3 = 6 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (3 = 7 ∈ ℤ)
12. ↑e ∈b Rcv
13. (f e) = 3 ∈ ℤ
14. ↑e ∈b Rcv
15. ¬↑e ∈b Send
16. ¬↑e ∈b Sign
17. ¬↑e ∈b Verify
18. ¬↑e ∈b Encrypt
19. ¬↑e ∈b Decrypt
⊢ ((↑e ∈b New) ∧ (¬a#New(e):Atom1)) ∨ (¬a#Rcv(e):SecurityData) ⇐⇒ (a ∈ sdata-atoms(Rcv(e)))
4
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ⟶ ℤ
6. (↑e ∈b New) ⇒ (6 = 1 ∈ ℤ)
7. (↑e ∈b Send) ⇒ (6 = 2 ∈ ℤ)
8. (↑e ∈b Rcv) ⇒ (6 = 3 ∈ ℤ)
9. (↑e ∈b Sign) ⇒ (6 = 4 ∈ ℤ)
10. (↑e ∈b Verify) ⇒ (6 = 5 ∈ ℤ)
11. (↑e ∈b Decrypt) ⇒ (6 = 7 ∈ ℤ)
12. ↑e ∈b Encrypt
13. (f e) = 6 ∈ ℤ
14. ¬↑e ∈b Rcv
15. ¬↑e ∈b Sign
16. ↑e ∈b Encrypt
17. ¬↑e ∈b Send
18. ¬↑e ∈b Verify
⊢ ((↑e ∈b New) ∧ (¬a#New(e):Atom1))
∨ (¬a#Encrypt(e):SecurityData × Key × Atom1)
∨ ((↑e ∈b Decrypt) ∧ (¬a#Decrypt(e):SecurityData × Key × Atom1))
⇐⇒ (a = cipherText(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e)))
5
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : Act@i
4. a : Atom1@i
5. f : E ⟶ ℤ
6. (↑e ∈b New) ⇒ (7 = 1 ∈ ℤ)
7. (↑e ∈b Send) ⇒ (7 = 2 ∈ ℤ)
8. (↑e ∈b Rcv) ⇒ (7 = 3 ∈ ℤ)
9. (↑e ∈b Sign) ⇒ (7 = 4 ∈ ℤ)
10. (↑e ∈b Verify) ⇒ (7 = 5 ∈ ℤ)
11. (↑e ∈b Encrypt) ⇒ (7 = 6 ∈ ℤ)
12. ↑e ∈b Decrypt
13. (f e) = 7 ∈ ℤ
14. ¬↑e ∈b Rcv
15. ¬↑e ∈b Sign
16. ¬↑e ∈b Encrypt
17. ↑e ∈b Decrypt
18. ¬↑e ∈b Send
19. ¬↑e ∈b Verify
⊢ ((↑e ∈b New) ∧ (¬a#New(e):Atom1)) ∨ (¬a#Decrypt(e):SecurityData × Key × Atom1)
⇐⇒ (a ∈ sdata-atoms(plainText(e))) ∨ (a ∈ [cipherText(e) / encryption-key-atoms(key(e))])
6
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)))
7
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))])
Latex:
Latex:
\mforall{}s:SES
(ActionsDisjoint
{}\mRightarrow{} (\mforall{}es:EO+(Info). \mforall{}e:Act. \mforall{}a:Atom1. ((e has a) \mLeftarrow{}{}\mRightarrow{} (a \mmember{} UseableAtoms(e)) \mvee{} (a \mmember{} UsedAtoms(e)))))
By
Latex:
(RepeatFor 5 ((D 0 THENA Auto))
THEN RepUR ``event-has class-value-has ses-useable-atoms ses-used-atoms`` 0
THEN Unfold `ses-disjoint` 2
THEN ((InstHyp [\mkleeneopen{}es\mkleeneclose{}] 2\mcdot{} THENM (Thin 2 THEN D -1)) THENA Auto)
THEN ((InstHyp [\mkleeneopen{}e\mkleeneclose{}] (-1)\mcdot{} THENM Thin (-2)) THENA Auto)
THEN (Assert Action(e) BY
(DVar `e' THEN Unhide THEN Auto))
THEN SplitAndHyps
THEN Unfold `ses-action` -1
THEN SplitOrHyps
THEN ThinTrivial
THEN SplitAndHyps
THEN ThinTrivial
THEN Eliminate \mkleeneopen{}f e\mkleeneclose{}\mcdot{}
THEN Repeat (UnitProgress(((SplitOnConclITE THENA Auto)
THEN Try ((ThinTrivial
THEN (Trivial
ORELSE ArithGuard ((MoveToConcl (-1)
THEN All Thin
THEN Auto))\mcdot{}
)
))
))\mcdot{})
THEN Reduce 0
THEN (RWW "nil\_member member\_singleton" 0 THENA Auto)
THEN (RW (SweepUpC BasicSimpC) 0 THENA Auto))
Home
Index