Nuprl Lemma : CRX-authentication-theorem
∀sth:SecurityTheory
(CRX-protocol{i:l}(sth-es(sth)) |= CR-initiator4{i:l}(sth-es(sth)) authenticates 2 messages
∧ CRX-protocol{i:l}(sth-es(sth)) |= CR-responder6{i:l}(sth-es(sth)) authenticates 3 messages )
Proof
Definitions occuring in Statement :
CRX-protocol: CRX-protocol{i:l}(s),
CR-responder6: CR-responder6{i:l}(s),
CR-initiator4: CR-initiator4{i:l}(s),
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-initiator4_wf,
ses-thread-loc_wf,
ses-thread_wf,
ses-honest_wf,
not_wf,
equal_wf,
Id_wf,
CRX-protocol_wf,
event-ordering+_wf,
ses-info_wf,
CR-responder6_wf,
security-theory_wf,
CRX-protocol-legal,
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,
ses-basic-sequence1_wf,
CR-initiator1_wf,
cons_wf,
CR-initiator2_wf,
CR-responder4_wf,
CR-responder5_wf,
nil_wf,
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,
atom-sdata_wf,
sdata-pair_wf,
id-sdata_wf,
id-sdata-not-pair2,
id-sdata-one-one,
atom-sdata-one-one,
nonce-release-lemma2,
l_exists_iff,
l_member_wf,
cons_member,
l_exists_wf,
iff_weakening_equal,
es-loc_wf,
event-has*-iff,
sdata-has-atom,
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,
and_wf,
sdata_atoms_pair_lemma,
matching-conversation_wf,
le_wf,
list-cases,
stuck-spread,
base_wf,
product_subtype_list,
non_neg_length,
length_wf_nat,
equal-wf-T-base,
list_wf,
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,
iseg_length,
iseg_select2,
iseg_same_length,
subtype_rel_list,
pi2_wf,
id-sdata-not-pair
Latex:
\mforall{}sth:SecurityTheory
(CRX-protocol\{i:l\}(sth-es(sth)) |= CR-initiator4\{i:l\}(sth-es(sth)) authenticates 2 messages
\mwedge{} CRX-protocol\{i:l\}(sth-es(sth)) |= CR-responder6\{i:l\}(sth-es(sth)) authenticates 3 messages )
Date html generated:
2015_07_23-PM-00_24_46
Last ObjectModification:
2015_02_04-PM-04_35_37
Home
Index