---

Step * 1 of Lemma ses-nonce-from-ordering


1. s : SES@i'
2. ActionsDisjoint@i'
3. PropertyO@i'
4. ses-ordering'(s)
⊢ PropertyN
BY
{ ((UnfoldTopAb (-1) THEN UnfoldTopAb 0) THEN RepeatFor 4 ((D 0 THENA Auto))) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. PropertyO@i'
4. ∀es:EO+(Info). ∀b:E.
     ((∀n:E(New). (b has* New(n) ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
     ∧ (∀e1:E(Sign)
          (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))))))))
     ∧ (∀e1:E(Encrypt)
          (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)))))))))
5. es : EO+(Info)@i'
6. n : E(New)@i
7. e : E@i
8. e has* New(n)@i
⊢ n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  PropertyO@i'
4.  ses-ordering'(s)
\mvdash{}  PropertyN


By

---

Latex:
((UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0)  THEN  RepeatFor  4  ((D  0  THENA  Auto)))

---

Home Index