---

Step * 1 2 2 1 1 of Lemma ses-legal-thread-decrypt


1. s : SES@i'
2. ActionsDisjoint@i'
3. NoncesCiphersAndKeysDisjoint
4. PropertyD@i'
5. es : EO+(Info)@i'
6. A : Id@i
7. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
8. e : E@i
9. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
10. ↑e ∈b Decrypt
11. i : ℕ||thr||@i
12. e = thr[i] ∈ E@i
13. ∀a:Atom1. ((a ∈ UsedAtoms(thr[i])) ⇒ (a ∈ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]))
14. l : Atom1 List
15. y : {x:ℤ| (0 ≤ x) ∧ x < i} 
16. (y ∈ [0, i))
17. l = UseableAtoms(thr[y]) ∈ (Atom1 List)
18. (cipherText(e) ∈ l)
⊢ ∃a:Act. ((a <loc e) ∧ (∃i:ℕ||thr||. (a = thr[i] ∈ E)) ∧ (a has cipherText(e)))
BY
{ ((Assert thr[y] ∈ Act BY Auto) THEN With ⌈thr[y]⌉ (D 0)⋅ THEN Auto) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. NoncesCiphersAndKeysDisjoint
4. PropertyD@i'
5. es : EO+(Info)@i'
6. A : Id@i
7. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
8. e : E@i
9. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
10. ↑e ∈b Decrypt
11. i : ℕ||thr||@i
12. e = thr[i] ∈ E@i
13. ∀a:Atom1. ((a ∈ UsedAtoms(thr[i])) ⇒ (a ∈ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]))
14. l : Atom1 List
15. y : {x:ℤ| (0 ≤ x) ∧ x < i} 
16. (y ∈ [0, i))
17. l = UseableAtoms(thr[y]) ∈ (Atom1 List)
18. (cipherText(e) ∈ l)
19. thr[y] ∈ Act
⊢ (thr[y] <loc e)

2
1. s : SES@i'
2. ActionsDisjoint@i'
3. NoncesCiphersAndKeysDisjoint
4. PropertyD@i'
5. es : EO+(Info)@i'
6. A : Id@i
7. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
8. e : E@i
9. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
10. ↑e ∈b Decrypt
11. i : ℕ||thr||@i
12. e = thr[i] ∈ E@i
13. ∀a:Atom1. ((a ∈ UsedAtoms(thr[i])) ⇒ (a ∈ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]))
14. l : Atom1 List
15. y : {x:ℤ| (0 ≤ x) ∧ x < i} 
16. (y ∈ [0, i))
17. l = UseableAtoms(thr[y]) ∈ (Atom1 List)
18. (cipherText(e) ∈ l)
19. thr[y] ∈ Act
20. (thr[y] <loc e)
⊢ ∃i:ℕ||thr||. (thr[y] = thr[i] ∈ E)

3
1. s : SES@i'
2. ActionsDisjoint@i'
3. NoncesCiphersAndKeysDisjoint
4. PropertyD@i'
5. es : EO+(Info)@i'
6. A : Id@i
7. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
8. e : E@i
9. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
10. ↑e ∈b Decrypt
11. i : ℕ||thr||@i
12. e = thr[i] ∈ E@i
13. ∀a:Atom1. ((a ∈ UsedAtoms(thr[i])) ⇒ (a ∈ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]))
14. l : Atom1 List
15. y : {x:ℤ| (0 ≤ x) ∧ x < i} 
16. (y ∈ [0, i))
17. l = UseableAtoms(thr[y]) ∈ (Atom1 List)
18. (cipherText(e) ∈ l)
19. thr[y] ∈ Act
20. (thr[y] <loc e)
21. ∃i:ℕ||thr||. (thr[y] = thr[i] ∈ E)
⊢ (thr[y] has cipherText(e))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  NoncesCiphersAndKeysDisjoint
4.  PropertyD@i'
5.  es  :  EO+(Info)@i'
6.  A  :  Id@i
7.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\}  @i
8.  e  :  E@i
9.  \mforall{}i:\mBbbN{}||thr||.  UsedAtoms(thr[i])  \msubseteq{}  [Private(A)  /  concat(map(\mlambda{}j.UseableAtoms(thr[j]);[0,  i)))]@i
10.  \muparrow{}e  \mmember{}\msubb{}  Decrypt
11.  i  :  \mBbbN{}||thr||@i
12.  e  =  thr[i]@i
13.  \mforall{}a:Atom1
            ((a  \mmember{}  UsedAtoms(thr[i]))  {}\mRightarrow{}  (a  \mmember{}  [Private(A)  /  concat(map(\mlambda{}j.UseableAtoms(thr[j]);[0,  i)))]))
14.  l  :  Atom1  List
15.  y  :  \{x:\mBbbZ{}|  (0  \mleq{}  x)  \mwedge{}  x  <  i\} 
16.  (y  \mmember{}  [0,  i))
17.  l  =  UseableAtoms(thr[y])
18.  (cipherText(e)  \mmember{}  l)
\mvdash{}  \mexists{}a:Act.  ((a  <loc  e)  \mwedge{}  (\mexists{}i:\mBbbN{}||thr||.  (a  =  thr[i]))  \mwedge{}  (a  has  cipherText(e)))


By

---

Latex:
((Assert  thr[y]  \mmember{}  Act  BY  Auto)  THEN  With  \mkleeneopen{}thr[y]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index