---

Step * 1 of Lemma ses-signature-unique


1. s : SES
2. PropertyO
3. es : EO+(Info)
4. a : E(Sign)@i
5. ∀a1:E(Sign)
     ((a1 < a)
     ⇒ (∀b:E(Sign). ((signature(a1) = signature(b) ∈ Atom1) ⇒ (Sign(a1) = Sign(b) ∈ (SecurityData × Id × Atom1)))))
6. b : E(Sign)@i
7. signature(a) = signature(b) ∈ Atom1@i
⊢ Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1)
BY
{ ((With ⌈es⌉ (D 2)⋅ THENA Auto) THEN ExRepD THEN (InstHyp [⌈b⌉;⌈a⌉] (-2)⋅ THENA Auto)) }

1
.....antecedent..... 
1. s : SES
2. es : EO+(Info)
3. a : E(Sign)@i
4. ∀a1:E(Sign)
     ((a1 < a)
     ⇒ (∀b:E(Sign). ((signature(a1) = signature(b) ∈ Atom1) ⇒ (Sign(a1) = Sign(b) ∈ (SecurityData × Id × Atom1)))))
5. b : E(Sign)@i
6. signature(a) = signature(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)))))
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)))))))
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)))))))
⊢ (a has signature(b))

2
1. s : SES
2. es : EO+(Info)
3. a : E(Sign)@i
4. ∀a1:E(Sign)
     ((a1 < a)
     ⇒ (∀b:E(Sign). ((signature(a1) = signature(b) ∈ Atom1) ⇒ (Sign(a1) = Sign(b) ∈ (SecurityData × Id × Atom1)))))
5. b : E(Sign)@i
6. signature(a) = signature(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)))))
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)))))))
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)))))))
10. ∃e2:E(Sign)
     ((Sign(e2) = Sign(b) ∈ (SecurityData × Id × Atom1))
     ∧ (e2 ≤loc a  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < a) ∧ snd has* signature(b)))))
⊢ Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1)

---

Latex:

---

Latex:

1.  s  :  SES
2.  PropertyO
3.  es  :  EO+(Info)
4.  a  :  E(Sign)@i
5.  \mforall{}a1:E(Sign).  ((a1  <  a)  {}\mRightarrow{}  (\mforall{}b:E(Sign).  ((signature(a1)  =  signature(b))  {}\mRightarrow{}  (Sign(a1)  =  Sign(b)))))
6.  b  :  E(Sign)@i
7.  signature(a)  =  signature(b)@i
\mvdash{}  Sign(a)  =  Sign(b)


By

---

Latex:
((With  \mkleeneopen{}es\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))

---

Home Index