src/HOL/Auth/OtwayRees_AN.ML
changeset 2106 1a52e2c5897e
parent 2090 307ebbbec862
child 2131 3106a99d30a5
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Oct 18 11:39:10 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Oct 18 11:39:55 1996 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4  
     1.5  (**** Inductive proofs about otway ****)
     1.6  
     1.7 +(*Monotonicity*)
     1.8  goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
     1.9  by (rtac subsetI 1);
    1.10  by (etac otway.induct 1);
    1.11 @@ -188,18 +189,6 @@
    1.12  qed "new_nonces_not_seen";
    1.13  Addsimps [new_nonces_not_seen];
    1.14  
    1.15 -(*Another variant: old messages must contain old nonces!*)
    1.16 -goal thy 
    1.17 - "!!evs. [| Says A B X : set_of_list evs;  \
    1.18 -\           Nonce (newN evt) : parts {X};    \
    1.19 -\           evs : otway lost                 \
    1.20 -\        |] ==> length evt < length evs";
    1.21 -by (rtac ccontr 1);
    1.22 -by (dtac leI 1);
    1.23 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
    1.24 -                      addIs  [impOfSubs parts_mono]) 1);
    1.25 -qed "Says_imp_old_nonces";
    1.26 -
    1.27  
    1.28  (*Nobody can have USED keys that will be generated in the future.
    1.29    ...very like new_keys_not_seen*)
    1.30 @@ -210,19 +199,13 @@
    1.31  (*OR1 and OR3*)
    1.32  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
    1.33  (*Fake, OR2, OR4: these messages send unknown (X) components*)
    1.34 -by (EVERY 
    1.35 -    (map
    1.36 -     (best_tac
    1.37 +by (REPEAT
    1.38 +    (best_tac
    1.39        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.40                        impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.41                        Suc_leD]
    1.42                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
    1.43 -               addss (!simpset)))
    1.44 -     [3,2,1]));
    1.45 -(*Reveal: dummy message*)
    1.46 -by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
    1.47 -                      addIs  [less_SucI, impOfSubs keysFor_mono]
    1.48 -                      addss (!simpset addsimps [le_def])) 1);
    1.49 +               addss (!simpset)) 1));
    1.50  val lemma = result();
    1.51  
    1.52  goal thy 
    1.53 @@ -287,25 +270,6 @@
    1.54  ****)
    1.55  
    1.56  
    1.57 -(*NOT useful in this form, but it says that session keys are not used
    1.58 -  to encrypt messages containing other keys, in the actual protocol.
    1.59 -  We require that agents should behave like this subsequently also.*)
    1.60 -goal thy 
    1.61 - "!!evs. evs : otway lost ==> \
    1.62 -\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
    1.63 -\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
    1.64 -by (etac otway.induct 1);
    1.65 -by parts_Fake_tac;
    1.66 -by (ALLGOALS Asm_simp_tac);
    1.67 -(*Deals with Faked messages*)
    1.68 -by (best_tac (!claset addSEs partsEs
    1.69 -                      addDs [impOfSubs parts_insert_subset_Un]
    1.70 -                      addss (!simpset)) 2);
    1.71 -(*Base case and Reveal*)
    1.72 -by (Auto_tac());
    1.73 -result();
    1.74 -
    1.75 -
    1.76  (** Session keys are not used to encrypt other session keys **)
    1.77  
    1.78  (*The equality makes the induction hypothesis easier to apply*)
    1.79 @@ -323,7 +287,7 @@
    1.80                           @ pushes)
    1.81                 setloop split_tac [expand_if])));
    1.82  (** LEVEL 5 **)
    1.83 -(*Reveal case 2, OR4, OR2, Fake*) 
    1.84 +(*Reveal case 2, OR4, Fake*) 
    1.85  by (EVERY (map spy_analz_tac [6, 4, 2]));
    1.86  (*Reveal case 1, OR3, Base*)
    1.87  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
    1.88 @@ -407,7 +371,8 @@
    1.89  (*Corollary: if A receives B's OR4 message and the nonce NA agrees
    1.90    then the key really did come from the Server!  CANNOT prove this of the
    1.91    bad form of this protocol, even though we can prove
    1.92 -  Spy_not_see_encrypted_key*)
    1.93 +  Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
    1.94 +  the Server's message from its nonce NA.)*)
    1.95  goal thy 
    1.96   "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
    1.97  \            : set_of_list evs;                                         \
    1.98 @@ -465,10 +430,10 @@
    1.99  (*Reveal case 2, OR4, Fake*) 
   1.100  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.101  (*Reveal case 1*) (** LEVEL 6 **)
   1.102 -by (excluded_middle_tac "Aa : lost" 1);
   1.103 +by (case_tac "Aa : lost" 1);
   1.104  (*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.105 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   1.106 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   1.107 +by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.108 +by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.109  (*So now we have  Aa ~: lost *)
   1.110  by (dtac A_trust_OR4 1);
   1.111  by (REPEAT (assume_tac 1));
   1.112 @@ -476,8 +441,8 @@
   1.113  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.114  
   1.115  goal thy 
   1.116 - "!!evs. [| Says Server B \
   1.117 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.118 + "!!evs. [| Says Server B                                                     \
   1.119 +\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                     \
   1.120  \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   1.121  \           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.122  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.123 @@ -488,9 +453,9 @@
   1.124  
   1.125  
   1.126  goal thy 
   1.127 - "!!evs. [| C ~: {A,B,Server};                                           \
   1.128 -\           Says Server B \
   1.129 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.130 + "!!evs. [| C ~: {A,B,Server};                                                \
   1.131 +\           Says Server B                                                     \
   1.132 +\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                     \
   1.133  \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   1.134  \           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.135  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.136 @@ -506,9 +471,9 @@
   1.137  
   1.138  (*If the encrypted message appears then it originated with the Server!*)
   1.139  goal thy 
   1.140 - "!!evs. [| B ~: lost;  evs : otway lost |]                   \
   1.141 -\    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)       \
   1.142 -\         : parts (sees lost Spy evs)                         \
   1.143 + "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   1.144 +\    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)                     \
   1.145 +\         : parts (sees lost Spy evs)                                       \
   1.146  \        --> (EX NA. Says Server B                                          \
   1.147  \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   1.148  \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   1.149 @@ -523,10 +488,10 @@
   1.150  (*Guarantee for B: if it gets a message with matching NB then the Server
   1.151    has sent the correct message.*)
   1.152  goal thy 
   1.153 - "!!evs. [| B ~: lost;  evs : otway lost;               \
   1.154 -\           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
   1.155 -\            : set_of_list evs |]                                  \
   1.156 -\        ==> EX NA. Says Server B                                          \
   1.157 + "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   1.158 +\           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}  \
   1.159 +\            : set_of_list evs |]                                           \
   1.160 +\        ==> EX NA. Says Server B                                           \
   1.161  \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   1.162  \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   1.163  \                     : set_of_list evs";