---

{ s:SES. es:EO+(Info).
    [P:E  E  Atom1  ]
      ((e1,e2:E. a:Atom1.
          (((e1 has a)  (e2 has a)  e1 loc e2 )  P[e1;e2;a]))
       (e1,e2:E. snd:E(Send). rcv:E(Rcv). a:Atom1.
            ((e1 c snd
             rcv c e2
             (snd < rcv)
             (Send(snd) = Rcv(rcv))
             P[e1;snd;a]
             P[rcv;e2;a])
             P[e1;e2;a]))
       (e1,e2:E. encr:E(Encrypt). decr:E(Decrypt). a:Atom1.
            (((e1 <loc encr)
             decr c e2
             (encr < decr)
             ((plainText(decr) = plainText(encr))
               (cipherText(decr) = cipherText(encr))
               MatchingKeys(key(decr);key(encr)))
             ((key(decr) = symmetric-key(a)))
             P[e1;encr;a]
             P[encr;decr;cipherText(encr)]
             P[decr;e2;a])
             P[e1;e2;a]))
       {e1,e2:E. a:Atom1.  (ses-flow(s;es;a;e1;e2)  P[e1;e2;a])}) }

{ Proof }

---

Definitions occuring in Statement :  ses-flow: ses-flow(s;es;a;e1;e2),  event-has: (e has a),  ses-key-rel: MatchingKeys(k1;k2),  ses-cipher: cipherText(e),  ses-decryption-key: key(e),  ses-decrypted: plainText(e),  ses-decrypt: Decrypt,  ses-crypt: cipherText(e),  ses-encryption-key: key(e),  ses-encrypted: plainText(e),  ses-encrypt: Encrypt,  ses-rcv: Rcv,  ses-send: Send,  ses-info: Info,  security-event-structure: SES,  symmetric-key: symmetric-key(a),  encryption-key: Key,  sdata: SecurityData,  es-E-interface: E(X),  eclass-val: X(e),  event-ordering+: EO+(Info),  es-causle: e c e',  es-le: e loc e' ,  es-locl: (e <loc e'),  es-causl: (e < e'),  es-E: E,  uall: [x:A]. B[x],  prop: ,  guard: {T},  so_apply: x[s1;s2;s3],  all: x:A. B[x],  not: A,  implies: P  Q,  and: P  Q,  function: x:A  B[x],  equal: s = t,  atom: Atom$n
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  and: P  Q,  so_apply: x[s1;s2;s3],  member: t  T,  cand: A c B,  assert: b,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  top: Top,  es-E-interface: E(X),  guard: {T},  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T),  subtype: S  T
Lemmas :  ses-flow-implies',  es-causle_wf,  es-causl_wf,  sdata_wf,  eclass-val_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  ses-send_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  ses-rcv_wf,  ses-flow_wf,  es-E-interface_wf,  es-interface-subtype_rel2,  ses-info_wf,  top_wf,  es-locl_wf,  ses-decrypted_wf,  ses-encrypted_wf,  ses-cipher_wf,  ses-crypt_wf,  ses-key-rel_wf,  ses-decryption-key_wf,  ses-encryption-key_wf,  not_wf,  encryption-key_wf,  symmetric-key_wf,  ses-decrypt_wf,  ses-encrypt_wf,  event-has_wf,  es-le_wf,  security-event-structure_wf,  assert_elim,  in-eclass_wf

---

\mforall{}s:SES.  \mforall{}es:EO+(Info).
    \mforall{}[P:E  {}\mrightarrow{}  E  {}\mrightarrow{}  Atom1  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}e1,e2:E.  \mforall{}a:Atom1.    (((e1  has  a)  \mwedge{}  (e2  has  a)  \mwedge{}  e1  \mleq{}loc  e2  )  {}\mRightarrow{}  P[e1;e2;a]))
        {}\mRightarrow{}  (\mforall{}e1,e2:E.  \mforall{}snd:E(Send).  \mforall{}rcv:E(Rcv).  \mforall{}a:Atom1.
                    ((e1  c\mleq{}  snd
                    \mwedge{}  rcv  c\mleq{}  e2
                    \mwedge{}  (snd  <  rcv)
                    \mwedge{}  (Send(snd)  =  Rcv(rcv))
                    \mwedge{}  P[e1;snd;a]
                    \mwedge{}  P[rcv;e2;a])
                    {}\mRightarrow{}  P[e1;e2;a]))
        {}\mRightarrow{}  (\mforall{}e1,e2:E.  \mforall{}encr:E(Encrypt).  \mforall{}decr:E(Decrypt).  \mforall{}a:Atom1.
                    (((e1  <loc  encr)
                    \mwedge{}  decr  c\mleq{}  e2
                    \mwedge{}  (encr  <  decr)
                    \mwedge{}  ((plainText(decr)  =  plainText(encr))
                        \mwedge{}  (cipherText(decr)  =  cipherText(encr))
                        \mwedge{}  MatchingKeys(key(decr);key(encr)))
                    \mwedge{}  (\mneg{}(key(decr)  =  symmetric-key(a)))
                    \mwedge{}  P[e1;encr;a]
                    \mwedge{}  P[encr;decr;cipherText(encr)]
                    \mwedge{}  P[decr;e2;a])
                    {}\mRightarrow{}  P[e1;e2;a]))
        {}\mRightarrow{}  \{\mforall{}e1,e2:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;e1;e2)  {}\mRightarrow{}  P[e1;e2;a])\})


Date html generated: 2011_08_17-PM-07_19_58
Last ObjectModification: 2011_06_18-PM-01_12_24

Home Index