Nuprl Lemma : ses-encrypted_wf

[s:SES]. ∀[es:EO+(Info)]. ∀[e:E(Encrypt)].  (plainText(e) ∈ SecurityData)


Proof




Definitions occuring in Statement :  ses-encrypted: plainText(e) ses-encrypt: Encrypt ses-info: Info security-event-structure: SES sdata: SecurityData es-E-interface: E(X) event-ordering+: EO+(Info) uall: [x:A]. B[x] member: t ∈ T
Lemmas :  eclass-val_wf sdata_wf encryption-key_wf es-E_wf event-ordering+_subtype ses-encrypt_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base es-E-interface_wf ses-info_wf es-interface-subtype_rel2 event-ordering+_wf top_wf subtype_top security-event-structure_wf

Latex:
\mforall{}[s:SES].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E(Encrypt)].    (plainText(e)  \mmember{}  SecurityData)



Date html generated: 2015_07_23-PM-00_03_17
Last ObjectModification: 2015_01_29-AM-07_45_28

Home Index