Step
*
1
1
1
1
of Lemma
ses-cipher-unique
.....equality.....
1. s : SES@i'
2. es : EO+(Info)@i'
3. a : E(Encrypt)@i
4. ∀a1:E(Encrypt)
((a1 < a)
⇒ (∀b:E(Encrypt)
((cipherText(a1) = cipherText(b) ∈ Atom1)
⇒ (Encrypt(a1) = Encrypt(b) ∈ (SecurityData × Key × Atom1)))))
5. b : E(Encrypt)@i
6. cipherText(a) = cipherText(b) ∈ Atom1@i
7. ∀n:E(New). ∀e:E. ((e has New(n))
⇒ (n ≤loc e ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n)))))@i'
8. ∀e1:E(Sign). ∀b:E.
((b has signature(e1))
⇒ (∃e2:E(Sign)
((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1)))))))@i'
9. ∀e1:E(Encrypt). ∀b:E.
((b has cipherText(e1))
⇒ (∃e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
∧ (e2 ≤loc b ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))@i'
10. ↑a ∈b Encrypt
11. cipherText(b)#Encrypt(a):SecurityData × Key × Atom1@i
⊢ Encrypt(a) ~ <plainText(a), key(a), cipherText(a)>
BY
{ (RepUR ``ses-encrypted ses-encryption-key ses-crypt`` 0
THEN (GenConclAtAddr [1] THENA Auto)
THEN RepeatFor 2 (D -2)
THEN Reduce 0
THEN Auto)⋅ }
Latex:
Latex:
.....equality.....
1. s : SES@i'
2. es : EO+(Info)@i'
3. a : E(Encrypt)@i
4. \mforall{}a1:E(Encrypt)
((a1 < a) {}\mRightarrow{} (\mforall{}b:E(Encrypt). ((cipherText(a1) = cipherText(b)) {}\mRightarrow{} (Encrypt(a1) = Encrypt(b)))))
5. b : E(Encrypt)@i
6. cipherText(a) = cipherText(b)@i
7. \mforall{}n:E(New). \mforall{}e:E.
((e has New(n))
{}\mRightarrow{} (n \mleq{}loc e \mvee{} (\mexists{}snd:E(Send). ((n <loc snd) \mwedge{} (snd < e) \mwedge{} snd has* New(n)))))@i'
8. \mforall{}e1:E(Sign). \mforall{}b:E.
((b has signature(e1))
{}\mRightarrow{} (\mexists{}e2:E(Sign)
((Sign(e2) = Sign(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* signature(e1)))))))@i'
9. \mforall{}e1:E(Encrypt). \mforall{}b:E.
((b has cipherText(e1))
{}\mRightarrow{} (\mexists{}e2:E(Encrypt)
((Encrypt(e2) = Encrypt(e1))
\mwedge{} (e2 \mleq{}loc b
\mvee{} (\mexists{}snd:E(Send). ((e2 <loc snd) \mwedge{} (snd < b) \mwedge{} snd has* cipherText(e1)))))))@i'
10. \muparrow{}a \mmember{}\msubb{} Encrypt
11. cipherText(b)\#Encrypt(a):SecurityData \mtimes{} Key \mtimes{} Atom1@i
\mvdash{} Encrypt(a) \msim{} <plainText(a), key(a), cipherText(a)>
By
Latex:
(RepUR ``ses-encrypted ses-encryption-key ses-crypt`` 0
THEN (GenConclAtAddr [1] THENA Auto)
THEN RepeatFor 2 (D -2)
THEN Reduce 0
THEN Auto)\mcdot{}
Home
Index