---

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


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))))
BY
{ ((InstHyp [⌈es⌉;⌈e⌉] 4⋅ THENA Auto) THEN D -1 THEN Thin (-1) THEN (InstHyp [⌈n⌉] (-1)⋅ THENA Auto) THEN D -1) }

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
9. ∀n:E(New). (e has* New(n) ⇒ (n ≤loc e  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n)))))
10. n ≤loc e 
⊢ n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))

2
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
9. ∀n:E(New). (e has* New(n) ⇒ (n ≤loc e  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n)))))
10. ∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n))
⊢ 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.  \mforall{}es:EO+(Info).  \mforall{}b:E.
          ((\mforall{}n:E(New)
                  (b  has*  New(n)
                  {}\mRightarrow{}  (n  \mleq{}loc  b    \mvee{}  (\mexists{}snd:E(Send).  ((n  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  New(n))))))
          \mwedge{}  (\mforall{}e1:E(Sign)
                    (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))))))))
          \mwedge{}  (\mforall{}e1:E(Encrypt)
                    (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)))))))))
5.  es  :  EO+(Info)@i'
6.  n  :  E(New)@i
7.  e  :  E@i
8.  e  has*  New(n)@i
\mvdash{}  n  c\mleq{}  e  \mwedge{}  ((\mneg{}(loc(e)  =  loc(n)))  {}\mRightarrow{}  (\mexists{}e':E(Send).  ((n  <loc  e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  (e'  <  e))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index