Nuprl Lemma : CR-authentication-theorem
∀sth:SecurityTheory
(CR-protocol |= CR-initiator3 authenticates 2 messages ∧ CR-protocol |= CR-responder3 authenticates 3 messages )
Proof
Definitions occuring in Statement :
CR-protocol: CR-protocol,
CR-responder3: CR-responder3,
CR-initiator3: CR-initiator3,
authentication: prtcl |= bs authenticates n messages ,
sth-es: sth-es(s),
security-theory: SecurityTheory,
all: ∀x:A. B[x],
and: P ∧ Q,
natural_number: $n
Lemmas :
sth-axioms,
ses-axioms-imply,
sth-es_wf,
ses-D-implies,
is-basic-seq_wf,
CR-initiator3_wf,
ses-thread-loc_wf,
ses-thread_wf,
ses-honest_wf,
not_wf,
equal_wf,
Id_wf,
CR-protocol_wf,
event-ordering+_wf,
ses-info_wf,
CR-responder3_wf,
security-theory_wf,
CR-protocol-legal,
CR-protocol-fresh,
signature-release-lemma2,
cons_wf,
ses-basic-sequence1_wf,
CR-initiator1_wf,
CR-initiator2_wf,
CR-responder1_wf,
CR-responder2_wf,
nil_wf,
l_exists_iff,
l_member_wf,
cons_member,
l_exists_wf,
list_ind_cons_lemma,
list_ind_nil_lemma,
length_of_cons_lemma,
length_of_nil_lemma,
sq_stable__all,
int_seg_wf,
subtract_wf,
es-locl_wf,
event-ordering+_subtype,
select_wf,
ses-act_wf,
sq_stable__le,
decidable__lt,
length_wf,
false_wf,
less-iff-le,
condition-implies-le,
add-associates,
minus-add,
minus-one-mul,
add-swap,
add-commutes,
add_functionality_wrt_le,
le-add-cancel2,
decidable__le,
not-le-2,
zero-add,
add-zero,
le-add-cancel,
sq_stable_from_decidable,
decidable__es-locl,
squash_wf,
subtype_base_sq,
int_subtype_base,
lelt_wf,
le_antisymmetry_iff,
assert_wf,
in-eclass_wf,
ses-verify_wf,
es-interface-subtype_rel2,
es-E_wf,
top_wf,
subtype_top,
sdata_wf,
product_subtype_base,
sdata_subtype_base,
atom2_subtype_base,
atom1_subtype_base,
sq_stable__assert,
ses-sign_wf,
ses-decrypt_wf,
encryption-key_wf,
ses-encrypt_wf,
ses-rcv_wf,
ses-send_wf,
ses-new_wf,
ses-action_wf,
l_exists_cons,
l_exists_nil,
int_seg_properties,
decidable__equal_int,
less_than_wf,
equal-wf-base,
eclass-val_wf,
assert_functionality_wrt_uiff,
true_wf,
eclass_wf,
sdata-pair-one-one,
sdata-pair_wf,
id-sdata_wf,
atom-sdata_wf,
atom-sdata-one-one,
id-sdata-one-one,
nonce-release-lemma2,
iff_weakening_equal,
es-loc_wf,
event-has*-iff,
sdata-has-atom,
sdata_atoms_pair_lemma,
sdata_atoms_atom_lemma,
or_wf,
class-value-has_wf,
exists_wf,
infix_ap_wf,
ses-info-flow_wf,
subtype_rel_dep_function,
event-has*_wf,
iseg_same_length,
iseg_weakening,
iseg_wf,
iseg_select2,
es-locl_transitivity2,
es-le_weakening_eq,
subtype_rel_list,
list_wf,
es-le_weakening,
es-causl_transitivity2,
es-causl_weakening,
es-causle_weakening,
es-causle_weakening_locl,
es-causl_irreflexivity,
iseg_length,
equal_functionality_wrt_subtype_rel2,
and_wf,
matching-conversation_wf,
le_wf,
list-cases,
stuck-spread,
base_wf,
product_subtype_list,
non_neg_length,
length_wf_nat,
equal-wf-T-base,
filter_cons_lemma,
filter_nil_lemma,
ses-msg-cases,
zip_cons_cons_lemma,
zip_nil_lemma,
send-rcv-match_wf,
l_all-nil,
l_all_cons,
l_all_wf2,
pi2_wf,
free-from-atom_wf
Latex:
\mforall{}sth:SecurityTheory
(CR-protocol |= CR-initiator3 authenticates 2 messages
\mwedge{} CR-protocol |= CR-responder3 authenticates 3 messages )
Date html generated:
2015_07_23-PM-00_23_48
Last ObjectModification:
2015_02_04-PM-04_22_33
Home
Index