src/HOL/Auth/Yahalom.ML
changeset 3516 470626799511
parent 3501 4ab477ffb4c6
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Jul 11 13:30:01 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jul 11 13:32:39 1997 +0200
     1.3 @@ -34,16 +34,6 @@
     1.4  
     1.5  (**** Inductive proofs about yahalom ****)
     1.6  
     1.7 -(*Monotonicity*)
     1.8 -goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
     1.9 -by (rtac subsetI 1);
    1.10 -by (etac yahalom.induct 1);
    1.11 -by (REPEAT_FIRST
    1.12 -    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    1.13 -                              :: yahalom.intrs))));
    1.14 -qed "yahalom_mono";
    1.15 -
    1.16 -
    1.17  (*Nobody sends themselves messages*)
    1.18  goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
    1.19  by (etac yahalom.induct 1);
    1.20 @@ -267,34 +257,14 @@
    1.21  qed "Spy_not_see_encrypted_key";
    1.22  
    1.23  
    1.24 -(*And other agents don't see the key either.*)
    1.25 -goal thy 
    1.26 - "!!evs. [| C ~: {A,B,Server};                                    \
    1.27 -\           Says Server A                                         \
    1.28 -\              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.29 -\                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.30 -\             : set evs;                                          \
    1.31 -\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
    1.32 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    1.33 -\        ==> Key K ~: analz (sees lost C evs)";
    1.34 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    1.35 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    1.36 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    1.37 -by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
    1.38 -qed "Agent_not_see_encrypted_key";
    1.39 -
    1.40 -
    1.41  (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
    1.42    It simplifies the proof by discarding needless information about
    1.43  	analz (insert X (sees lost Spy evs)) 
    1.44  *)
    1.45 -val analz_mono_parts_induct_tac = 
    1.46 -    etac yahalom.induct 1 
    1.47 +fun analz_mono_parts_induct_tac i = 
    1.48 +    etac yahalom.induct i
    1.49      THEN 
    1.50 -    REPEAT_FIRST  
    1.51 -      (rtac impI THEN' 
    1.52 -       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
    1.53 -       mp_tac)  
    1.54 +    REPEAT_FIRST analz_mono_contra_tac
    1.55      THEN  parts_sees_tac;
    1.56  
    1.57  
    1.58 @@ -346,7 +316,7 @@
    1.59  \                                  Nonce NA, Nonce NB|},                \
    1.60  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
    1.61  \                       : set evs)";
    1.62 -by analz_mono_parts_induct_tac;
    1.63 +by (analz_mono_parts_induct_tac 1);
    1.64  (*YM3 & Fake*)
    1.65  by (Blast_tac 2);
    1.66  by (Fake_parts_insert_tac 1);
    1.67 @@ -517,7 +487,7 @@
    1.68  \       : parts(sees lost Spy evs)                   \
    1.69  \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
    1.70  \       ~: parts(sees lost Spy evs)";
    1.71 -by analz_mono_parts_induct_tac;
    1.72 +by (analz_mono_parts_induct_tac 1);
    1.73  by (Fake_parts_insert_tac 1);
    1.74  by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
    1.75                         addSIs [parts_insertI]
    1.76 @@ -672,19 +642,6 @@
    1.77  
    1.78  (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
    1.79  
    1.80 -(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
    1.81 -  It simplifies the proof by discarding needless information about
    1.82 -	analz (insert X (sees lost Spy evs)) 
    1.83 -*)
    1.84 -val analz_mono_parts_induct_tac = 
    1.85 -    etac yahalom.induct 1 
    1.86 -    THEN 
    1.87 -    REPEAT_FIRST  
    1.88 -      (rtac impI THEN' 
    1.89 -       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
    1.90 -       mp_tac)  
    1.91 -    THEN  parts_sees_tac;
    1.92 -
    1.93  (*Assuming the session key is secure, if both certificates are present then
    1.94    A has said NB.  We can't be sure about the rest of A's message, but only
    1.95    NB matters for freshness.*)  
    1.96 @@ -696,7 +653,7 @@
    1.97  \              : parts (sees lost Spy evs) -->                          \
    1.98  \            B ~: lost -->                                              \
    1.99  \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.100 -by analz_mono_parts_induct_tac;
   1.101 +by (analz_mono_parts_induct_tac 1);
   1.102  (*Fake*)
   1.103  by (Fake_parts_insert_tac 1);
   1.104  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)