src/HOL/Auth/OtwayRees.ML
changeset 2194 63a68a3a8a76
parent 2171 91b4161a28e5
child 2214 f869dc885841
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Nov 18 16:30:06 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Nov 18 16:34:37 1996 +0100
     1.3 @@ -493,18 +493,18 @@
     1.4  (**** Authenticity properties relating to NB ****)
     1.5  
     1.6  (*Only OR2 can have caused such a part of a message to appear.  We do not
     1.7 -  know anything about X'.*)
     1.8 +  know anything about X: it does NOT have to have the right form.*)
     1.9  goal thy 
    1.10   "!!evs. [| B ~: lost;  evs : otway lost |]                    \
    1.11  \        ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B)       \
    1.12  \             : parts (sees lost Spy evs) -->                  \
    1.13 -\            (EX X'. Says B Server                             \
    1.14 -\             {|NA, Agent A, Agent B, X',                      \
    1.15 +\            (EX X. Says B Server                              \
    1.16 +\             {|NA, Agent A, Agent B, X,                       \
    1.17  \               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
    1.18  \             : set_of_list evs)";
    1.19  by (parts_induct_tac 1);
    1.20  by (auto_tac (!claset, !simpset addcongs [conj_cong]));
    1.21 -qed_spec_mp "Crypt_imp_OR2";
    1.22 +bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
    1.23  
    1.24  
    1.25  (** The Nonce NB uniquely identifies B's  message. **)
    1.26 @@ -556,12 +556,9 @@
    1.27                        addSEs partsEs
    1.28                        addEs [Says_imp_old_nonces RS less_irrefl]
    1.29                        addss (!simpset)) 1);
    1.30 -(*OR3 and OR4*)  (** LEVEL 5 **)
    1.31  (*OR4*)
    1.32 -by (REPEAT (Safe_step_tac 2));
    1.33 -by (rtac (Crypt_imp_OR2 RS exE) 2);
    1.34 -by (REPEAT (fast_tac (!claset addEs partsEs) 2));
    1.35 -(*OR3*)  (** LEVEL 8 **)
    1.36 +by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
    1.37 +(*OR3*)
    1.38  by (step_tac (!claset delrules [disjCI, impCE]) 1);
    1.39  by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
    1.40  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
    1.41 @@ -598,36 +595,38 @@
    1.42  B_trust_OR3 RS Spy_not_see_encrypted_key;
    1.43  
    1.44  
    1.45 -(** A session key uniquely identifies a pair of senders in the message
    1.46 -    encrypted by a good agent C.  NEEDED?  INTERESTING?**)
    1.47  goal thy 
    1.48 - "!!evs. evs : otway lost ==>                                           \
    1.49 -\      EX A B. ALL C N.                                                 \
    1.50 -\         C ~: lost -->                                                 \
    1.51 -\         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) -->   \
    1.52 -\         C=A | C=B";
    1.53 -by (Simp_tac 1);        (*Miniscoping*)
    1.54 + "!!evs. [| B ~: lost;  evs : otway lost |]                    \
    1.55 +\        ==> Says Server B                                                 \
    1.56 +\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
    1.57 +\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
    1.58 +\            (EX X. Says B Server {|NA, Agent A, Agent B, X,              \
    1.59 +\                            Crypt {|NA, NB, Agent A, Agent B|}     \
    1.60 +\                                  (shrK B)|}                       \
    1.61 +\            : set_of_list evs)";
    1.62  by (etac otway.induct 1);
    1.63 -by analz_Fake_tac;
    1.64 -(*spy_analz_tac just does not work here: it is an entirely different proof!*)
    1.65 -by (ALLGOALS 
    1.66 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
    1.67 -                                      imp_conjR, parts_insert_sees,
    1.68 -                                      parts_insert2])));
    1.69 -by (REPEAT_FIRST (etac exE));
    1.70 -(*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
    1.71 -by (expand_case_tac "K = ?y" 4);
    1.72 -by (REPEAT (ares_tac [exI] 5));
    1.73 -(*...we prove this case by contradiction: the key is too new!*)
    1.74 -by (fast_tac (!claset addSEs partsEs
    1.75 -                      addEs [Says_imp_old_keys RS less_irrefl]
    1.76 -                      addss (!simpset)) 4);
    1.77 -(*Base, Fake, OR2, OR4*)
    1.78 -by (REPEAT_FIRST ex_strip_tac);
    1.79 -by (dtac synth.Inj 4);
    1.80 -by (dtac synth.Inj 3);
    1.81 -(*Now in effect there are three Fake cases*)
    1.82 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
    1.83 -                                    delrules [disjCI, disjE]
    1.84 -                                    addss (!simpset))));
    1.85 -qed "key_identifies_senders";
    1.86 +by (Auto_tac());
    1.87 +bd (Says_imp_sees_Spy RS parts.Inj) 1;
    1.88 +by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
    1.89 +bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
    1.90 +
    1.91 +
    1.92 +(*After getting and checking OR4, agent A can trust that B has been active.
    1.93 +  We could probably prove that X has the expected form, but that is not
    1.94 +  strictly necessary for authentication.*)
    1.95 +goal thy 
    1.96 + "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
    1.97 +\            : set_of_list evs;                                    \
    1.98 +\           Says A B {|NA, Agent A, Agent B,                       \
    1.99 +\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
   1.100 +\            : set_of_list evs;                                    \
   1.101 +\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   1.102 +\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   1.103 +\                            Crypt {|NA, NB, Agent A, Agent B|}    \
   1.104 +\                                  (shrK B)|}                      \
   1.105 +\            : set_of_list evs";
   1.106 +by (fast_tac (!claset addSDs  [A_trust_OR4]
   1.107 +	              addSEs [OR3_imp_OR2]) 1);
   1.108 +qed "A_auths_B";
   1.109 +
   1.110 +