Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
authorpaulson
Mon Jun 22 15:53:24 1998 +0200 (1998-06-22)
changeset 506630271d90644f
parent 5065 99abb086212e
child 5067 62b6288e6005
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.

The former format was just a hack to invoke type distinctions, while the
latter uses the explictness principle.
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Mon Jun 22 15:50:59 1998 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Mon Jun 22 15:53:24 1998 +0200
     1.3 @@ -17,6 +17,11 @@
     1.4  set proof_timing;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 +AddEs spies_partsEs;
     1.8 +AddDs [impOfSubs analz_subset_parts];
     1.9 +AddDs [impOfSubs Fake_parts_insert];
    1.10 +
    1.11 +
    1.12  (*A "possibility property": there are traces that reach the end*)
    1.13  goal thy 
    1.14   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.15 @@ -54,8 +59,7 @@
    1.16  (*Relates to both YM4 and Oops*)
    1.17  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
    1.18  \                K : parts (spies evs)";
    1.19 -by (blast_tac (claset() addSEs partsEs
    1.20 -                        addSDs [Says_imp_spies RS parts.Inj]) 1);
    1.21 +by (Blast_tac 1);
    1.22  qed "YM4_Key_parts_spies";
    1.23  
    1.24  (*For proving the easier theorems about X ~: parts (spies evs).*)
    1.25 @@ -81,14 +85,13 @@
    1.26  goal thy 
    1.27   "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.28  by (parts_induct_tac 1);
    1.29 -by (Fake_parts_insert_tac 1);
    1.30 -by (Blast_tac 1);
    1.31 +by (ALLGOALS Blast_tac);
    1.32  qed "Spy_see_shrK";
    1.33  Addsimps [Spy_see_shrK];
    1.34  
    1.35  goal thy 
    1.36   "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.37 -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    1.38 +by Auto_tac;
    1.39  qed "Spy_analz_shrK";
    1.40  Addsimps [Spy_analz_shrK];
    1.41  
    1.42 @@ -101,7 +104,7 @@
    1.43  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    1.44  by (parts_induct_tac 1);
    1.45  (*YM4: Key K is not fresh!*)
    1.46 -by (blast_tac (claset() addSEs spies_partsEs) 3);
    1.47 +by (Blast_tac 3);
    1.48  (*YM3*)
    1.49  by (blast_tac (claset() addss (simpset())) 2);
    1.50  (*Fake*)
    1.51 @@ -148,8 +151,8 @@
    1.52  (** Session keys are not used to encrypt other session keys **)
    1.53  
    1.54  goal thy  
    1.55 - "!!evs. evs : yahalom ==>                                  \
    1.56 -\  ALL K KK. KK <= Compl (range shrK) -->                   \
    1.57 + "!!evs. evs : yahalom ==>                               \
    1.58 +\  ALL K KK. KK <= Compl (range shrK) -->                \
    1.59  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    1.60  \            (K : KK | Key K : analz (spies evs))";
    1.61  by (etac yahalom.induct 1);
    1.62 @@ -162,7 +165,7 @@
    1.63  qed_spec_mp "analz_image_freshK";
    1.64  
    1.65  goal thy
    1.66 - "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>        \
    1.67 + "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>     \
    1.68  \        Key K : analz (insert (Key KAB) (spies evs)) =  \
    1.69  \        (K = KAB | Key K : analz (spies evs))";
    1.70  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    1.71 @@ -184,8 +187,7 @@
    1.72  by (expand_case_tac "K = ?y" 1);
    1.73  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.74  (*...we assume X is a recent message and handle this case by contradiction*)
    1.75 -by (blast_tac (claset() addSEs spies_partsEs
    1.76 -                        delrules [conjI]    (*prevent splitup into 4 subgoals*)
    1.77 +by (blast_tac (claset() delrules [conjI]    (*prevent splitup into 4 subgoals*)
    1.78                          addss (simpset() addsimps [parts_insertI])) 1);
    1.79  val lemma = result();
    1.80  
    1.81 @@ -203,11 +205,11 @@
    1.82  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
    1.83  
    1.84  goal thy 
    1.85 - "!!evs. [| A ~: bad;  B ~: bad;  A ~= B;                     \
    1.86 + "!!evs. [| A ~: bad;  B ~: bad;  A ~= B;                       \
    1.87  \           evs : yahalom |]                                    \
    1.88  \        ==> Says Server A                                      \
    1.89  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
    1.90 -\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
    1.91 +\                    Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
    1.92  \             : set evs -->                                     \
    1.93  \            Notes Spy {|na, nb, Key K|} ~: set evs -->         \
    1.94  \            Key K ~: analz (spies evs)";
    1.95 @@ -220,9 +222,7 @@
    1.96  (*Oops*)
    1.97  by (blast_tac (claset() addDs [unique_session_keys]) 3);
    1.98  (*YM3*)
    1.99 -by (blast_tac (claset() delrules [impCE]
   1.100 -                        addSEs spies_partsEs
   1.101 -                        addIs [impOfSubs analz_subset_parts]) 2);
   1.102 +by (blast_tac (claset() delrules [impCE]) 2);
   1.103  (*Fake*) 
   1.104  by (spy_analz_tac 1);
   1.105  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.106 @@ -232,7 +232,7 @@
   1.107  goal thy 
   1.108   "!!evs. [| Says Server A                                    \
   1.109  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
   1.110 -\                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
   1.111 +\                    Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}    \
   1.112  \           : set evs;                                       \
   1.113  \           Notes Spy {|na, nb, Key K|} ~: set evs;          \
   1.114  \           A ~: bad;  B ~: bad;  evs : yahalom |]           \
   1.115 @@ -252,12 +252,11 @@
   1.116  \           A ~: bad;  evs : yahalom |]                                \
   1.117  \         ==> EX nb. Says Server A                                     \
   1.118  \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   1.119 -\                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
   1.120 +\                            Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
   1.121  \                    : set evs";
   1.122  by (etac rev_mp 1);
   1.123  by (parts_induct_tac 1);
   1.124 -by (Fake_parts_insert_tac 1);
   1.125 -by (Blast_tac 1);
   1.126 +by (ALLGOALS Blast_tac);
   1.127  qed "A_trusts_YM3";
   1.128  
   1.129  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   1.130 @@ -273,20 +272,19 @@
   1.131  (** Security Guarantee for B upon receiving YM4 **)
   1.132  
   1.133  (*B knows, by the first part of A's message, that the Server distributed 
   1.134 -  the key for A and B, and has associated it with NB. *)
   1.135 +  the key for A and B, and has associated it with NB.*)
   1.136  goal thy 
   1.137 - "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} : parts (spies evs); \
   1.138 -\           B ~: bad;  evs : yahalom |]                             \
   1.139 -\        ==> EX NA. Says Server A                                    \
   1.140 -\                    {|Nonce NB,                                     \
   1.141 -\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
   1.142 -\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
   1.143 -\                       : set evs";
   1.144 + "!!evs. [| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
   1.145 +\             : parts (spies evs);                               \
   1.146 +\           B ~: bad;  evs : yahalom |]                          \
   1.147 +\ ==> EX NA. Says Server A                                       \
   1.148 +\               {|Nonce NB,                                      \
   1.149 +\                 Crypt (shrK A) {|Agent B, Key K, Nonce NA|},   \
   1.150 +\                 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \
   1.151 +\               : set evs";
   1.152  by (etac rev_mp 1);
   1.153  by (parts_induct_tac 1);
   1.154 -by (Fake_parts_insert_tac 1);
   1.155 -(*YM3*)
   1.156 -by (Blast_tac 1);
   1.157 +by (ALLGOALS Blast_tac);
   1.158  qed "B_trusts_YM4_shrK";
   1.159  
   1.160  
   1.161 @@ -296,25 +294,26 @@
   1.162  (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   1.163    because we do not have to show that NB is secret. *)
   1.164  goal thy 
   1.165 - "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
   1.166 -\             : set evs;                                                 \
   1.167 -\           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
   1.168 -\        ==> EX NA. Says Server A                                        \
   1.169 -\                    {|Nonce NB,                                         \
   1.170 -\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
   1.171 -\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
   1.172 -\                   : set evs";
   1.173 -by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   1.174 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   1.175 +\                       X|}                                         \
   1.176 +\             : set evs;                                            \
   1.177 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                  \
   1.178 +\ ==> EX NA. Says Server A                                          \
   1.179 +\               {|Nonce NB,                                         \
   1.180 +\                 Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
   1.181 +\                 Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \
   1.182 +\              : set evs";
   1.183  by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1);
   1.184  qed "B_trusts_YM4";
   1.185  
   1.186  
   1.187  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   1.188  goal thy 
   1.189 - "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
   1.190 -\             : set evs;                                                 \
   1.191 -\           ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs;        \
   1.192 -\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
   1.193 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   1.194 +\                       X|}                                         \
   1.195 +\             : set evs;                                            \
   1.196 +\           ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs;   \
   1.197 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                  \
   1.198  \        ==> Key K ~: analz (spies evs)";
   1.199  by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
   1.200  qed "B_gets_good_key";
   1.201 @@ -325,37 +324,36 @@
   1.202  
   1.203  (*The encryption in message YM2 tells us it cannot be faked.*)
   1.204  goal thy 
   1.205 - "!!evs. evs : yahalom                                                  \
   1.206 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs) -->  \
   1.207 -\      B ~: bad -->                                                    \
   1.208 -\      (EX NB. Says B Server {|Agent B, Nonce NB,                       \
   1.209 -\                              Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   1.210 -\         : set evs)";
   1.211 + "!!evs. [| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs);  \
   1.212 +\           B ~: bad;  evs : yahalom                                   \
   1.213 +\        |] ==> EX NB. Says B Server {|Agent B, Nonce NB,              \
   1.214 +\                               Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   1.215 +\                        : set evs";
   1.216 +by (etac rev_mp 1);
   1.217 +by (etac rev_mp 1);
   1.218  by (parts_induct_tac 1);
   1.219 -by (Fake_parts_insert_tac 1);
   1.220 -(*YM2*)
   1.221 -by (Blast_tac 1);
   1.222 -bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   1.223 +by (ALLGOALS Blast_tac);
   1.224 +qed "B_Said_YM2";
   1.225  
   1.226  
   1.227  (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   1.228  goal thy 
   1.229 - "!!evs. evs : yahalom                                                   \
   1.230 -\  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   1.231 -\         : set evs -->                                                  \
   1.232 -\      B ~: bad -->                                                     \
   1.233 -\      (EX nb'. Says B Server {|Agent B, nb',                            \
   1.234 -\                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   1.235 -\                 : set evs)";
   1.236 + "!!evs. [| Says Server A                                              \
   1.237 +\               {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   1.238 +\             : set evs;                                               \
   1.239 +\           B ~: bad;  evs : yahalom                                   \
   1.240 +\        |] ==> EX nb'. Says B Server {|Agent B, nb',                  \
   1.241 +\                               Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   1.242 +\                         : set evs";
   1.243 +by (etac rev_mp 1);
   1.244 +by (etac rev_mp 1);
   1.245  by (etac yahalom.induct 1);
   1.246  by (ALLGOALS Asm_simp_tac);
   1.247  (*YM3*)
   1.248 -by (blast_tac (claset() addSDs [B_Said_YM2]
   1.249 - 		        addSEs [MPair_parts]
   1.250 -	 	        addDs [Says_imp_spies RS parts.Inj]) 3);
   1.251 +by (blast_tac (claset() addSDs [B_Said_YM2]) 3);
   1.252  (*Fake, YM2*)
   1.253  by (ALLGOALS Blast_tac);
   1.254 -val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   1.255 +val lemma = result();
   1.256  
   1.257  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.258  goal thy
   1.259 @@ -365,8 +363,7 @@
   1.260  \   ==> EX nb'. Says B Server                                               \
   1.261  \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   1.262  \                 : set evs";
   1.263 -by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   1.264 -		        addEs spies_partsEs) 1);
   1.265 +by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]) 1);
   1.266  qed "YM3_auth_B_to_A";
   1.267  
   1.268  
   1.269 @@ -374,45 +371,41 @@
   1.270  
   1.271  (*Assuming the session key is secure, if both certificates are present then
   1.272    A has said NB.  We can't be sure about the rest of A's message, but only
   1.273 -  NB matters for freshness.*)  
   1.274 +  NB matters for freshness.  Note that  Key K ~: analz (spies evs)  must be
   1.275 +  the FIRST antecedent of the induction formula.*)  
   1.276  goal thy 
   1.277 - "!!evs. evs : yahalom                                        \
   1.278 + "!!evs. evs : yahalom                                     \
   1.279  \        ==> Key K ~: analz (spies evs) -->                \
   1.280  \            Crypt K (Nonce NB) : parts (spies evs) -->    \
   1.281 -\            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}      \
   1.282 +\            Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}      \
   1.283  \              : parts (spies evs) -->                     \
   1.284 -\            B ~: bad -->                                    \
   1.285 +\            B ~: bad -->                                  \
   1.286  \            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.287  by (parts_induct_tac 1);
   1.288  (*Fake*)
   1.289 -by (Fake_parts_insert_tac 1);
   1.290 +by (Blast_tac 1);
   1.291  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   1.292  by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
   1.293  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   1.294  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   1.295  (*yes: apply unicity of session keys*)
   1.296  by (not_bad_tac "Aa" 1);
   1.297 -by (blast_tac (claset() addSEs [MPair_parts]
   1.298 -			addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.299 -			addDs  [Says_imp_spies RS parts.Inj,
   1.300 -				unique_session_keys]) 1);
   1.301 -val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   1.302 +by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   1.303 +			addDs  [unique_session_keys]) 1);
   1.304 +qed_spec_mp "Auth_A_to_B_lemma";
   1.305 +
   1.306  
   1.307  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   1.308    Moreover, A associates K with NB (thus is talking about the same run).
   1.309    Other premises guarantee secrecy of K.*)
   1.310  goal thy 
   1.311 - "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   1.312 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
   1.313  \                       Crypt K (Nonce NB)|} : set evs;                 \
   1.314  \           (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   1.315  \           A ~: bad;  B ~: bad;  evs : yahalom |]                    \
   1.316  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.317 -by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   1.318 -by (dtac B_trusts_YM4_shrK 1);
   1.319 -by Safe_tac;
   1.320 -by (rtac lemma 1);
   1.321 -by (rtac Spy_not_see_encrypted_key 2);
   1.322 -by (REPEAT_FIRST assume_tac);
   1.323 -by (ALLGOALS (blast_tac (claset() addSEs [MPair_parts]
   1.324 -			          addDs [Says_imp_spies RS parts.Inj])));
   1.325 +by (subgoal_tac "Key K ~: analz (spies evs)" 1);
   1.326 +by (blast_tac (claset() addIs [Auth_A_to_B_lemma]) 1);
   1.327 +by (blast_tac (claset() addDs  [Spy_not_see_encrypted_key,
   1.328 +				B_trusts_YM4_shrK]) 1);
   1.329  qed_spec_mp "YM4_imp_A_Said_YM3";
     2.1 --- a/src/HOL/Auth/Yahalom2.thy	Mon Jun 22 15:50:59 1998 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom2.thy	Mon Jun 22 15:53:24 1998 +0200
     2.3 @@ -42,7 +42,7 @@
     2.4  
     2.5           (*The Server receives Bob's message.  He responds by sending a
     2.6             new session key to Alice, with a certificate for forwarding to Bob.
     2.7 -           Fields are reversed in the 2nd certificate to prevent attacks!! *)
     2.8 +           Both agents are quoted in the 2nd certificate to prevent attacks!*)
     2.9      YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
    2.10               Says B' Server {|Agent B, Nonce NB,
    2.11  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    2.12 @@ -50,7 +50,7 @@
    2.13            ==> Says Server A
    2.14                 {|Nonce NB, 
    2.15                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    2.16 -                 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
    2.17 +                 Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
    2.18                   # evs3 : yahalom"
    2.19  
    2.20           (*Alice receives the Server's (?) message, checks her Nonce, and