---

{ s:SES
    (ActionsDisjoint
     PropertyD
        (es:EO+(Info). A:Id. thr:Thread. e:E.
             (Legal(thr)@A
              e  thr
                 (a:Act. ((a <loc e)  a  thr  (a has cipherText(e)))) 
                supposing e  Decrypt)) 
       supposing NoncesCiphersAndKeysDisjoint) }

{ Proof }

---

Definitions occuring in Statement :  ses-legal-thread: Legal(thr)@A,  ses-thread-member: e  thr,  ses-thread: Thread,  ses-nonce-disjoint: NoncesCiphersAndKeysDisjoint,  ses-disjoint: ActionsDisjoint,  ses-D: PropertyD,  event-has: (e has a),  ses-act: Act,  ses-cipher: cipherText(e),  ses-decrypt: Decrypt,  ses-info: Info,  security-event-structure: SES,  in-eclass: e  X,  event-ordering+: EO+(Info),  es-locl: (e <loc e'),  es-E: E,  Id: Id,  assert: b,  uimplies: b supposing a,  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  and: P  Q
Definitions :  all: x:A. B[x],  implies: P  Q,  uimplies: b supposing a,  ses-nonce-disjoint: NoncesCiphersAndKeysDisjoint,  ses-thread: Thread,  ses-legal-thread: Legal(thr)@A,  assert: b,  ses-thread-member: e  thr,  exists: x:A. B[x],  and: P  Q,  member: t  T,  not: A,  false: False,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  top: Top,  subtype: S  T,  prop: ,  le: A  B,  cand: A c B,  es-E-interface: E(X),  or: P  Q,  int_seg: {i..j},  lelt: i  j < k,  squash: T,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  sq_type: SQType(T),  guard: {T},  l_contains: A  B,  l_all: (xL.P[x]),  rev_implies: P  Q,  iff: P  Q,  ses-act: Act,  ses-D: PropertyD
Lemmas :  eclass-val_wf,  ses-info_wf,  es-E_wf,  event-ordering+_wf,  ses-new_wf,  subtype_base_sq,  bool_subtype_base,  ses-sig_wf,  es-E-interface_wf,  ses-sign_wf,  es-interface-subtype_rel2,  sdata_wf,  Id_wf,  event-ordering+_inc,  top_wf,  ses-crypt_wf,  ses-encrypt_wf,  encryption-key_wf,  ses-private_wf,  assert_witness,  in-eclass_wf,  ses-decrypt_wf,  int_seg_wf,  length_wf1,  ses-act_wf,  select_wf,  assert_wf,  l_contains_wf,  ses-used-atoms_wf,  concat_wf,  map_wf,  le_wf,  from-upto_wf,  ses-useable-atoms_wf,  es-locl_wf,  ses-D_wf,  ses-nonce-disjoint_wf,  ses-disjoint_wf,  security-event-structure_wf,  assert_elim,  ses-cipher_wf,  l_member_wf,  member-used-atoms,  encryption-key-atoms_wf,  ses-decryption-key_wf,  ses-verify_wf,  ses-verify-sig_wf,  sdata-atoms_wf,  ses-verify-signed_wf,  ses-signed_wf,  ses-encrypted_wf,  ses-encryption-key_wf,  ses-send_wf,  cons_member,  member-concat,  member_map,  event-has_wf,  ses-thread-order,  squash_wf,  true_wf,  event_ordering_wf,  ses-act-has-atom,  list_subtype_base,  atom1_subtype_base

---

\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  PropertyD
          {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}A:Id.  \mforall{}thr:Thread.  \mforall{}e:E.
                      (Legal(thr)@A
                      {}\mRightarrow{}  e  \mmember{}  thr  {}\mRightarrow{}  (\mexists{}a:Act.  ((a  <loc  e)  \mwedge{}  a  \mmember{}  thr  \mwedge{}  (a  has  cipherText(e)))) 
                            supposing  \muparrow{}e  \mmember{}\msubb{}  Decrypt)) 
          supposing  NoncesCiphersAndKeysDisjoint)


Date html generated: 2011_08_17-PM-07_36_05
Last ObjectModification: 2011_06_18-PM-01_28_33

Home Index