src/HOL/Auth/OtwayRees.ML
changeset 2053 6c0594bfa726
parent 2048 bb54fbba0071
child 2064 5a5e508e2a2b
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Oct 01 18:10:33 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Oct 01 18:19:12 1996 +0200
     1.3 @@ -484,8 +484,8 @@
     1.4  qed_spec_mp"no_nonce_OR1_OR2";
     1.5  
     1.6  
     1.7 -(*If the encrypted message appears, and A has used Nonce NA to start a run,
     1.8 -  then it originated with the Server!*)
     1.9 +(*Crucial property: If the encrypted message appears, and A has used NA
    1.10 +  to start a run, then it originated with the Server!*)
    1.11  goal thy 
    1.12   "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
    1.13  \    ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs)      \
    1.14 @@ -528,46 +528,26 @@
    1.15  qed_spec_mp "NA_Crypt_imp_Server_msg";
    1.16  
    1.17  
    1.18 -(*Crucial property: if A receives B's OR4 message and the nonce NA agrees
    1.19 +(*Corollary: if A receives B's OR4 message and the nonce NA agrees
    1.20    then the key really did come from the Server!  CANNOT prove this of the
    1.21    bad form of this protocol, even though we can prove
    1.22    Spy_not_see_encrypted_key*)
    1.23  goal thy 
    1.24 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]             \
    1.25 -\        ==> Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}        \
    1.26 -\             : set_of_list evs -->                                \
    1.27 -\            Says A B {|NA, Agent A, Agent B,                      \
    1.28 -\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
    1.29 -\             : set_of_list evs -->                                \
    1.30 -\            (EX NB. Says Server B                                 \
    1.31 + "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
    1.32 +\            : set_of_list evs;                                    \
    1.33 +\           Says A B {|NA, Agent A, Agent B,                       \
    1.34 +\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
    1.35 +\            : set_of_list evs;                                    \
    1.36 +\           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
    1.37 +\        ==> EX NB. Says Server B                                  \
    1.38  \                     {|NA,                                        \
    1.39  \                       Crypt {|NA, Key K|} (shrK A),              \
    1.40  \                       Crypt {|NB, Key K|} (shrK B)|}             \
    1.41 -\                       : set_of_list evs)";
    1.42 -by (etac otway.induct 1);
    1.43 -by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
    1.44 -(*OR2*)
    1.45 -by (Fast_tac 3);
    1.46 -(*OR1: it cannot be a new Nonce, contradiction.*)
    1.47 -by (fast_tac (!claset addSIs [parts_insertI]
    1.48 -                      addEs [Says_imp_old_nonces RS less_irrefl]
    1.49 -                      addss (!simpset)) 2);
    1.50 -(*Fake, OR4*) (** LEVEL 4 **)
    1.51 -by (step_tac (!claset delrules [impCE]) 1);
    1.52 -by (ALLGOALS Asm_simp_tac);
    1.53 -by (Fast_tac 4);
    1.54 -by (fast_tac (!claset addSIs [Crypt_imp_OR1]
    1.55 -                      addEs  partsEs
    1.56 -                      addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
    1.57 -(** LEVEL 8 **)
    1.58 -(*Still subcases of Fake and OR4*)
    1.59 -by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.60 -                      addDs  [impOfSubs analz_subset_parts]) 1);
    1.61 +\                       : set_of_list evs";
    1.62  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.63                        addEs  partsEs
    1.64                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.65 -val A_can_trust = 
    1.66 -    result() RSN (2, rev_mp) RS mp |> standard;
    1.67 +qed "A_can_trust";
    1.68  
    1.69  
    1.70  (*Describes the form of K and NA when the Server sends this message.*)