Strengthened and streamlined the Yahalom proofs
authorpaulson
Mon Jun 09 10:21:38 1997 +0200 (1997-06-09)
changeset 343204412cfe6861
parent 3431 05b397185e1d
child 3433 2de17c994071
Strengthened and streamlined the Yahalom proofs
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Jun 09 10:21:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Jun 09 10:21:38 1997 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1996  University of Cambridge
     1.6  
     1.7 -Inductive relation "otway" for the Yahalom protocol.
     1.8 +Inductive relation "yahalom" for the Yahalom protocol.
     1.9  
    1.10  From page 257 of
    1.11    Burrows, Abadi and Needham.  A Logic of Authentication.
    1.12 @@ -113,7 +113,7 @@
    1.13  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.14  
    1.15  
    1.16 -(*Nobody can have used non-existent keys!*)
    1.17 +(*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
    1.18  goal thy "!!evs. evs : yahalom lost ==>          \
    1.19  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    1.20  by parts_induct_tac;
    1.21 @@ -268,7 +268,7 @@
    1.22  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.23  
    1.24  
    1.25 -(*Final version: Server's message in the most abstract form*)
    1.26 +(*Final version*)
    1.27  goal thy 
    1.28   "!!evs. [| Says Server A                                         \
    1.29  \              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
    1.30 @@ -282,6 +282,7 @@
    1.31  qed "Spy_not_see_encrypted_key";
    1.32  
    1.33  
    1.34 +(*And other agents don't see the key either.*)
    1.35  goal thy 
    1.36   "!!evs. [| C ~: {A,B,Server};                                    \
    1.37  \           Says Server A                                         \
     2.1 --- a/src/HOL/Auth/Yahalom2.ML	Mon Jun 09 10:21:05 1997 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom2.ML	Mon Jun 09 10:21:38 1997 +0200
     2.3 @@ -17,6 +17,10 @@
     2.4  proof_timing:=true;
     2.5  HOL_quantifiers := false;
     2.6  
     2.7 +(*Replacing the variable by a constant improves speed*)
     2.8 +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
     2.9 +
    2.10 +
    2.11  (*A "possibility property": there are traces that reach the end*)
    2.12  goal thy 
    2.13   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    2.14 @@ -36,8 +40,8 @@
    2.15  by (rtac subsetI 1);
    2.16  by (etac yahalom.induct 1);
    2.17  by (REPEAT_FIRST
    2.18 -    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    2.19 -                              :: yahalom.intrs))));
    2.20 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    2.21 +			       :: yahalom.intrs))));
    2.22  qed "yahalom_mono";
    2.23  
    2.24  
    2.25 @@ -55,7 +59,7 @@
    2.26  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    2.27  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    2.28  \                X : analz (sees lost Spy evs)";
    2.29 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    2.30 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    2.31  qed "YM4_analz_sees_Spy";
    2.32  
    2.33  bind_thm ("YM4_parts_sees_Spy",
    2.34 @@ -66,18 +70,20 @@
    2.35  \                  : set_of_list evs ==> \
    2.36  \                K : parts (sees lost Spy evs)";
    2.37  by (blast_tac (!claset addSEs partsEs
    2.38 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    2.39 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
    2.40  qed "YM4_Key_parts_sees_Spy";
    2.41  
    2.42  (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    2.43    We instantiate the variable to "lost" since leaving it as a Var would
    2.44    interfere with simplification.*)
    2.45 -val parts_induct_tac = 
    2.46 -    etac yahalom.induct 1 THEN 
    2.47 +val parts_sees_tac = 
    2.48      forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
    2.49      forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
    2.50      prove_simple_subgoals_tac  1;
    2.51  
    2.52 +val parts_induct_tac = 
    2.53 +    etac yahalom.induct 1 THEN parts_sees_tac;
    2.54 +
    2.55  
    2.56  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    2.57      sends messages containing X! **)
    2.58 @@ -108,7 +114,7 @@
    2.59  AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    2.60  
    2.61  
    2.62 -(*Nobody can have used non-existent keys!*)
    2.63 +(*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
    2.64  goal thy "!!evs. evs : yahalom lost ==>          \
    2.65  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    2.66  by parts_induct_tac;
    2.67 @@ -130,7 +136,6 @@
    2.68  
    2.69  Addsimps [new_keys_not_used, new_keys_not_analzd];
    2.70  
    2.71 -
    2.72  (*Describes the form of K when the Server sends this message.  Useful for
    2.73    Oops as well as main secrecy property.*)
    2.74  goal thy 
    2.75 @@ -240,9 +245,8 @@
    2.76                 setloop split_tac [expand_if])));
    2.77  (*YM3*)
    2.78  by (blast_tac (!claset delrules [impCE]
    2.79 -                      addSEs sees_Spy_partsEs
    2.80 -                      addIs [impOfSubs analz_subset_parts]
    2.81 -                      addss (!simpset addsimps [parts_insert2])) 2);
    2.82 +                       addSEs sees_Spy_partsEs
    2.83 +                       addIs [impOfSubs analz_subset_parts]) 2);
    2.84  (*OR4, Fake*) 
    2.85  by (REPEAT_FIRST spy_analz_tac);
    2.86  (*Oops*)
    2.87 @@ -250,7 +254,7 @@
    2.88  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    2.89  
    2.90  
    2.91 -(*Final version: Server's message in the most abstract form*)
    2.92 +(*Final version*)
    2.93  goal thy 
    2.94   "!!evs. [| Says Server A                                         \
    2.95  \              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
    2.96 @@ -264,6 +268,7 @@
    2.97  qed "Spy_not_see_encrypted_key";
    2.98  
    2.99  
   2.100 +(*And other agents don't see the key either.*)
   2.101  goal thy 
   2.102   "!!evs. [| C ~: {A,B,Server};                                    \
   2.103  \           Says Server A                                         \
   2.104 @@ -282,7 +287,8 @@
   2.105  
   2.106  (*** Security Guarantees for A and B ***)
   2.107  
   2.108 -(*If the encrypted message appears then it originated with the Server.*)
   2.109 +(*If the encrypted message appears then it originated with the Server.
   2.110 +  May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   2.111  goal thy
   2.112   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA|}                \
   2.113  \            : parts (sees lost Spy evs);                              \
   2.114 @@ -317,7 +323,7 @@
   2.115  qed "B_trusts_YM4_shrK";
   2.116  
   2.117  (*With this variant we don't bother to use the 2nd part of YM4 at all, since
   2.118 -  Nonce NB is available in the first part.  However the 2nd part does assure B
   2.119 +  Nonce NB is available in the first part.  However, the 2nd part does assure B
   2.120    of A's existence.*)
   2.121  
   2.122  (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   2.123 @@ -331,6 +337,125 @@
   2.124  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},     \
   2.125  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
   2.126  \                   : set_of_list evs";
   2.127 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
   2.128 +by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   2.129  by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
   2.130  qed "B_trusts_YM4";
   2.131 +
   2.132 +
   2.133 +
   2.134 +(*** Authenticating B to A ***)
   2.135 +
   2.136 +(*The encryption in message YM2 tells us it cannot be faked.*)
   2.137 +goal thy 
   2.138 + "!!evs. evs : yahalom lost                                            \
   2.139 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees lost Spy evs) -->  \
   2.140 +\      B ~: lost --> \
   2.141 +\      (EX NB. Says B Server {|Agent B, Nonce NB,                      \
   2.142 +\                              Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
   2.143 +\         : set_of_list evs)";
   2.144 +by parts_induct_tac;
   2.145 +by (Fake_parts_insert_tac 1);
   2.146 +(*YM2*)
   2.147 +by (Blast_tac 1);
   2.148 +bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   2.149 +
   2.150 +(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   2.151 +goal thy 
   2.152 + "!!evs. evs : yahalom lost                                       \
   2.153 +\  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   2.154 +\         : set_of_list evs -->                                          \
   2.155 +\      B ~: lost -->                                                     \
   2.156 +\      (EX nb'. Says B Server {|Agent B, nb',                            \
   2.157 +\                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   2.158 +\                 : set_of_list evs)";
   2.159 +by (etac yahalom.induct 1);
   2.160 +by (ALLGOALS Asm_simp_tac);
   2.161 +(*YM3*)
   2.162 +by (blast_tac (!claset addSDs [B_Said_YM2]
   2.163 +		       addSEs [MPair_parts]
   2.164 +		       addDs [Says_imp_sees_Spy' RS parts.Inj]) 3);
   2.165 +(*Fake, YM2*)
   2.166 +by (ALLGOALS Blast_tac);
   2.167 +bind_thm ("Says_Server_imp_B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   2.168 +
   2.169 +(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   2.170 +goal thy
   2.171 + "!!evs. [| Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
   2.172 +\                                X|}  : set_of_list evs;               \
   2.173 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]              \
   2.174 +\         ==> EX nb. Says B Server                                     \
   2.175 +\                     {|Agent B, nb, Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   2.176 +\                    : set_of_list evs";
   2.177 +by (blast_tac (!claset addSDs [A_trusts_YM3, Says_Server_imp_B_Said_YM2]
   2.178 +		       addEs sees_Spy_partsEs) 1);
   2.179 +qed "YM3_auth_B_to_A";
   2.180 +
   2.181 +
   2.182 +(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   2.183 +  It simplifies the proof by discarding needless information about
   2.184 +	analz (insert X (sees lost Spy evs)) 
   2.185 +*)
   2.186 +val analz_mono_parts_induct_tac = 
   2.187 +    etac yahalom.induct 1 
   2.188 +    THEN 
   2.189 +    REPEAT_FIRST  
   2.190 +      (rtac impI THEN' 
   2.191 +       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   2.192 +       mp_tac)  
   2.193 +    THEN  parts_sees_tac;
   2.194 +
   2.195 +fun lost_tac s =
   2.196 +    case_tac ("(" ^ s ^ ") : lost") THEN'
   2.197 +    SELECT_GOAL 
   2.198 +      (REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN
   2.199 +       REPEAT_DETERM (etac MPair_analz 1) THEN
   2.200 +       THEN_BEST_FIRST 
   2.201 +         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   2.202 +         (has_fewer_prems 1, size_of_thm)
   2.203 +         (Step_tac 1));
   2.204 +
   2.205 +
   2.206 +(*Assuming the session key is secure, if it is used to encrypt NB then
   2.207 +  A has said NB.  We can't be sure about the rest of A's message, but only
   2.208 +  NB matters for freshness.*)  
   2.209 +goal thy 
   2.210 + "!!evs. evs : yahalom lost                                             \
   2.211 +\        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   2.212 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   2.213 +\            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}                \
   2.214 +\              : parts (sees lost Spy evs) -->                          \
   2.215 +\             B ~: lost -->                                             \
   2.216 +\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
   2.217 +by analz_mono_parts_induct_tac;
   2.218 +(*Fake*)
   2.219 +by (Fake_parts_insert_tac 1);
   2.220 +(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   2.221 +by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   2.222 +(*YM4*)
   2.223 +by(Step_tac 1);
   2.224 +by (REPEAT (Blast_tac 2));
   2.225 +by (lost_tac "Aa" 1);
   2.226 +by (blast_tac (!claset addSEs [MPair_parts]
   2.227 +                       addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   2.228 +		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   2.229 +			       unique_session_keys]) 1);
   2.230 +val lemma = normalize_thm [RSspec, RSmp] (result());
   2.231 +
   2.232 +(*If B receives YM4 then A has used nonce NB (and therefore is alive).
   2.233 +  Other premises guarantee secrecy of K.*)
   2.234 +goal thy 
   2.235 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   2.236 +\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   2.237 +\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|}           \
   2.238 +\               ~: set_of_list evs);                                    \
   2.239 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   2.240 +\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
   2.241 +be (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1;
   2.242 +bd (B_trusts_YM4_shrK) 1;
   2.243 +by (safe_tac (!claset));
   2.244 +br lemma 1;
   2.245 +br Spy_not_see_encrypted_key 2;
   2.246 +by (REPEAT_FIRST assume_tac);
   2.247 +by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts]
   2.248 +			 addDs [Says_imp_sees_Spy' RS parts.Inj])));
   2.249 +qed_spec_mp "YM4_imp_A_Said_YM3";
     3.1 --- a/src/HOL/Auth/Yahalom2.thy	Mon Jun 09 10:21:05 1997 +0200
     3.2 +++ b/src/HOL/Auth/Yahalom2.thy	Mon Jun 09 10:21:38 1997 +0200
     3.3 @@ -6,8 +6,7 @@
     3.4  Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     3.5  
     3.6  This version trades encryption of NB for additional explicitness in YM3.
     3.7 -It also omits encryption in YM2.  The resulting protocol no longer guarantees
     3.8 -that the other agent is present.
     3.9 +Also in YM3, care is taken to make the two certificates distinct.
    3.10  
    3.11  From page 259 of
    3.12    Burrows, Abadi and Needham.  A Logic of Authentication.
    3.13 @@ -37,14 +36,16 @@
    3.14  	   the sender is, hence the A' in the sender field.*)
    3.15      YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
    3.16               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    3.17 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs
    3.18 -                : yahalom lost"
    3.19 +          ==> Says B Server 
    3.20 +                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    3.21 +                # evs : yahalom lost"
    3.22  
    3.23           (*The Server receives Bob's message.  He responds by sending a
    3.24             new session key to Alice, with a packet for forwarding to Bob.
    3.25 -           Fields are reversed in the 2nd packet to prevent attacks.*)
    3.26 +           !! Fields are reversed in the 2nd packet to prevent attacks!! *)
    3.27      YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    3.28 -             Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    3.29 +             Says B' Server {|Agent B, Nonce NB,
    3.30 +			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    3.31                 : set_of_list evs |]
    3.32            ==> Says Server A
    3.33                 {|Nonce NB,