---

Step * of Lemma ses-ordering-ordering'

∀s:SES. (PropertyO ⇒ ActionsDisjoint ⇒ ses-ordering'(s))
BY
{ (Auto
   THEN (UnfoldTopAb 0 THEN (D 0 THENA Auto))
   THEN Assert ⌜∀m:ℕ. ∀b:E.
                  ((∀n:E(New). ∀e':E.
                      (((e' has New(n)) ∧ (e' ->>^m b))
                      ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
                  ∧ (∀e1:E(Sign). ∀e':E.
                       (((e' has signature(e1)) ∧ (e' ->>^m b))
                       ⇒ (∃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). ∀e':E.
                       (((e' has cipherText(e1)) ∧ (e' ->>^m b))
                       ⇒ (∃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)))))))))⌝
   ⋅) }

1
.....assertion..... 
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
⊢ ∀m:ℕ. ∀b:E.
    ((∀n:E(New). ∀e':E.
        (((e' has New(n)) ∧ (e' ->>^m b))
        ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
    ∧ (∀e1:E(Sign). ∀e':E.
         (((e' has signature(e1)) ∧ (e' ->>^m b))
         ⇒ (∃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). ∀e':E.
         (((e' has cipherText(e1)) ∧ (e' ->>^m b))
         ⇒ (∃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)))))))))

2
1. s : SES@i'
2. PropertyO@i'
3. ActionsDisjoint@i'
4. es : EO+(Info)@i'
5. ∀m:ℕ. ∀b:E.
     ((∀n:E(New). ∀e':E.
         (((e' has New(n)) ∧ (e' ->>^m b))
         ⇒ (n ≤loc b  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < b) ∧ snd has* New(n))))))
     ∧ (∀e1:E(Sign). ∀e':E.
          (((e' has signature(e1)) ∧ (e' ->>^m b))
          ⇒ (∃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). ∀e':E.
          (((e' has cipherText(e1)) ∧ (e' ->>^m b))
          ⇒ (∃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)))))))))
⊢ ∀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)))))))))

---

Latex:

---

Latex:
\mforall{}s:SES.  (PropertyO  {}\mRightarrow{}  ActionsDisjoint  {}\mRightarrow{}  ses-ordering'(s))


By

---

Latex:
(Auto
  THEN  (UnfoldTopAb  0  THEN  (D  0  THENA  Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  \mforall{}b:E.
                                ((\mforall{}n:E(New).  \mforall{}e':E.
                                        (((e'  has  New(n))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
                                        {}\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).  \mforall{}e':E.
                                          (((e'  has  signature(e1))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
                                          {}\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).  \mforall{}e':E.
                                          (((e'  has  cipherText(e1))  \mwedge{}  (e'  rel\_exp(E;  ->>  m)  b))
                                          {}\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)))))))))\mkleeneclose{}\mcdot{})

---

Home Index