src/HOL/Auth/Yahalom_Bad.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 10833 c0844a30ea4e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Auth/Yahalom
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "yahalom" for the Yahalom protocol.
     7 
     8 From page 257 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 (*A "possibility property": there are traces that reach the end*)
    14 Goal "A ~= Server \
    15 \     ==> EX X NB K. EX evs: yahalom.          \
    16 \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    17 by (REPEAT (resolve_tac [exI,bexI] 1));
    18 by (rtac (yahalom.Nil RS 
    19           yahalom.YM1 RS yahalom.Reception RS
    20           yahalom.YM2 RS yahalom.Reception RS 
    21           yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
    22 by possibility_tac;
    23 result();
    24 
    25 Goal "[| Gets B X : set evs; evs : yahalom |] ==> EX A. Says A B X : set evs";
    26 by (etac rev_mp 1);
    27 by (etac yahalom.induct 1);
    28 by Auto_tac;
    29 qed "Gets_imp_Says";
    30 
    31 (*Must be proved separately for each protocol*)
    32 Goal "[| Gets B X : set evs; evs : yahalom |]  ==> X : knows Spy evs";
    33 by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    34 qed"Gets_imp_knows_Spy";
    35 AddDs [Gets_imp_knows_Spy RS parts.Inj];
    36 
    37 fun g_not_bad_tac s = 
    38   ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s;
    39 
    40 
    41 (**** Inductive proofs about yahalom ****)
    42 
    43 
    44 (** For reasoning about the encrypted portion of messages **)
    45 
    46 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    47 Goal "[| Gets A {|Crypt (shrK A) Y, X|} : set evs;  evs : yahalom |]  \
    48 \     ==> X : analz (knows Spy evs)";
    49 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    50 qed "YM4_analz_knows_Spy";
    51 
    52 bind_thm ("YM4_parts_knows_Spy",
    53           YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    54 
    55 (*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    56 fun parts_knows_Spy_tac i = 
    57   EVERY
    58    [ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
    59     prove_simple_subgoals_tac i];
    60 
    61 (*Induction for regularity theorems.  If induction formula has the form
    62    X ~: analz (knows Spy evs) --> ... then it shortens the proof by discarding
    63    needless information about analz (insert X (knows Spy evs))  *)
    64 fun parts_induct_tac i = 
    65     etac yahalom.induct i
    66     THEN 
    67     REPEAT (FIRSTGOAL analz_mono_contra_tac)
    68     THEN  parts_knows_Spy_tac i;
    69 
    70 
    71 (** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    72     sends messages containing X! **)
    73 
    74 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    75 Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
    76 by (parts_induct_tac 1);
    77 by (Fake_parts_insert_tac 1);
    78 by (ALLGOALS Blast_tac);
    79 qed "Spy_see_shrK";
    80 Addsimps [Spy_see_shrK];
    81 
    82 Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
    83 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    84 qed "Spy_analz_shrK";
    85 Addsimps [Spy_analz_shrK];
    86 
    87 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    88 	Spy_analz_shrK RSN (2, rev_iffD1)];
    89 
    90 
    91 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
    92 Goal "evs : yahalom ==>          \
    93 \      Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
    94 by (parts_induct_tac 1);
    95 (*Fake*)
    96 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    97 (*YM2-4: Because Key K is not fresh, etc.*)
    98 by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
    99 qed_spec_mp "new_keys_not_used";
   100 
   101 bind_thm ("new_keys_not_analzd",
   102           [analz_subset_parts RS keysFor_mono,
   103            new_keys_not_used] MRS contra_subsetD);
   104 
   105 Addsimps [new_keys_not_used, new_keys_not_analzd];
   106 
   107 
   108 (*For proofs involving analz.*)
   109 val analz_knows_Spy_tac = 
   110     ftac YM4_analz_knows_Spy 7 THEN assume_tac 7;
   111 
   112 (****
   113  The following is to prove theorems of the form
   114 
   115   Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   116   Key K : analz (knows Spy evs)
   117 
   118  A more general formula must be proved inductively.
   119 ****)
   120 
   121 (** Session keys are not used to encrypt other session keys **)
   122 
   123 Goal "evs : yahalom ==>                              \
   124 \  ALL K KK. KK <= - (range shrK) -->                \
   125 \         (Key K : analz (Key``KK Un (knows Spy evs))) = \
   126 \         (K : KK | Key K : analz (knows Spy evs))";
   127 by (etac yahalom.induct 1);
   128 by analz_knows_Spy_tac;
   129 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   130 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   131 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   132 (*Fake*) 
   133 by (spy_analz_tac 1);
   134 qed_spec_mp "analz_image_freshK";
   135 
   136 Goal "[| evs : yahalom;  KAB ~: range shrK |]                  \
   137 \      ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   138 \          (K = KAB | Key K : analz (knows Spy evs))";
   139 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   140 qed "analz_insert_freshK";
   141 
   142 
   143 (*** The Key K uniquely identifies the Server's  message. **)
   144 
   145 Goal "evs : yahalom ==>                                     \
   146 \   EX A' B' na' nb' X'. ALL A B na nb X.                   \
   147 \       Says Server A                                       \
   148 \        {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}   \
   149 \       : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   150 by (etac yahalom.induct 1);
   151 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   152 by (ALLGOALS Clarify_tac);
   153 by (ex_strip_tac 2);
   154 by (Blast_tac 2);
   155 (*Remaining case: YM3*)
   156 by (expand_case_tac "K = ?y" 1);
   157 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   158 (*...we assume X is a recent message and handle this case by contradiction*)
   159 by (blast_tac (claset() addSEs knows_Spy_partsEs
   160                         delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   161 val lemma = result();
   162 
   163 Goal "[| Says Server A                                                 \
   164 \         {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs;  \
   165 \       Says Server A'                                                 \
   166 \         {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
   167 \       evs : yahalom |]                                    \
   168 \    ==> A=A' & B=B' & na=na' & nb=nb'";
   169 by (prove_unique_tac lemma 1);
   170 qed "unique_session_keys";
   171 
   172 
   173 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   174 
   175 Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]                \
   176 \     ==> Says Server A                                        \
   177 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   178 \             Crypt (shrK B) {|Agent A, Key K|}|}              \
   179 \          : set evs -->                                       \
   180 \         Key K ~: analz (knows Spy evs)";
   181 by (etac yahalom.induct 1);
   182 by analz_knows_Spy_tac;
   183 by (ALLGOALS
   184     (asm_simp_tac 
   185      (simpset() addsimps split_ifs @ pushes @
   186                          [analz_insert_eq, analz_insert_freshK])));
   187 (*YM3*)
   188 by (blast_tac (claset() delrules [impCE]
   189                         addSEs knows_Spy_partsEs
   190                         addIs [impOfSubs analz_subset_parts]) 2);
   191 (*Fake*) 
   192 by (spy_analz_tac 1);
   193 val lemma = result() RS mp RSN(2,rev_notE);
   194 
   195 
   196 (*Final version*)
   197 Goal "[| Says Server A                                         \
   198 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   199 \             Crypt (shrK B) {|Agent A, Key K|}|}              \
   200 \          : set evs;                                          \
   201 \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   202 \     ==> Key K ~: analz (knows Spy evs)";
   203 by (blast_tac (claset() addSEs [lemma]) 1);
   204 qed "Spy_not_see_encrypted_key";
   205 
   206 
   207 (** Security Guarantee for A upon receiving YM3 **)
   208 
   209 (*If the encrypted message appears then it originated with the Server*)
   210 Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   211 \        A ~: bad;  evs : yahalom |]                          \
   212 \      ==> Says Server A                                      \
   213 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},      \
   214 \             Crypt (shrK B) {|Agent A, Key K|}|}             \
   215 \          : set evs";
   216 by (etac rev_mp 1);
   217 by (parts_induct_tac 1);
   218 by (Fake_parts_insert_tac 1);
   219 qed "A_trusts_YM3";
   220 
   221 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   222 Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   223 \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   224 \     ==> Key K ~: analz (knows Spy evs)";
   225 by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
   226 qed "A_gets_good_key";
   227 
   228 (** Security Guarantees for B upon receiving YM4 **)
   229 
   230 (*B knows, by the first part of A's message, that the Server distributed 
   231   the key for A and B.  But this part says nothing about nonces.*)
   232 Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs);  \
   233 \        B ~: bad;  evs : yahalom |]                                 \
   234 \     ==> EX NA NB. Says Server A                                    \
   235 \                     {|Crypt (shrK A) {|Agent B, Key K,             \
   236 \                                        Nonce NA, Nonce NB|},       \
   237 \                       Crypt (shrK B) {|Agent A, Key K|}|}          \
   238 \                    : set evs";
   239 by (etac rev_mp 1);
   240 by (parts_induct_tac 1);
   241 by (Fake_parts_insert_tac 1);
   242 (*YM3*)
   243 by (Blast_tac 1);
   244 qed "B_trusts_YM4_shrK";
   245 
   246 (** Up to now, the reasoning is similar to standard Yahalom.  Now the
   247     doubtful reasoning occurs.  We should not be assuming that an unknown
   248     key is secure, but the model allows us to: there is no Oops rule to
   249     let session keys go.*)
   250 
   251 (*B knows, by the second part of A's message, that the Server distributed 
   252   the key quoting nonce NB.  This part says nothing about agent names. 
   253   Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)
   254   the secrecy of NB.*)
   255 Goal "evs : yahalom                                          \
   256 \     ==> Key K ~: analz (knows Spy evs) -->                 \
   257 \         Crypt K (Nonce NB) : parts (knows Spy evs) -->     \
   258 \         (EX A B NA. Says Server A                          \
   259 \                     {|Crypt (shrK A) {|Agent B, Key K,     \
   260 \                               Nonce NA, Nonce NB|},        \
   261 \                       Crypt (shrK B) {|Agent A, Key K|}|}  \
   262 \                    : set evs)";
   263 by (parts_induct_tac 1);
   264 by (ALLGOALS Clarify_tac);
   265 (*YM3 & Fake*)
   266 by (Blast_tac 2);
   267 by (Fake_parts_insert_tac 1);
   268 (*YM4*)
   269 (*A is uncompromised because NB is secure*)
   270 by (g_not_bad_tac "A" 1);
   271 (*A's certificate guarantees the existence of the Server message*)
   272 by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj RS parts.Fst RS
   273 			       A_trusts_YM3]) 1);
   274 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   275 
   276 
   277 (*B's session key guarantee from YM4.  The two certificates contribute to a
   278   single conclusion about the Server's message. *)
   279 Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                    \
   280 \                 Crypt K (Nonce NB)|} : set evs;                       \
   281 \        Says B Server                                                  \
   282 \          {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
   283 \          : set evs;                                                   \
   284 \        A ~: bad;  B ~: bad;  evs : yahalom |]                         \
   285 \      ==> EX na nb. Says Server A                                      \
   286 \                  {|Crypt (shrK A) {|Agent B, Key K, na, nb|},         \
   287 \                    Crypt (shrK B) {|Agent A, Key K|}|}                \
   288 \            : set evs";
   289 by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN
   290     assume_tac 1 THEN dtac B_trusts_YM4_shrK 1);
   291 by (dtac B_trusts_YM4_newK 3);
   292 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   293 by (etac Spy_not_see_encrypted_key 1 THEN REPEAT (assume_tac 1));
   294 by (ftac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   295 by (blast_tac (claset() addDs []) 1);
   296 qed "B_trusts_YM4";
   297 
   298 
   299 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   300 Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                   \
   301 \                    Crypt K (Nonce NB)|} : set evs;                   \
   302 \        Says B Server                                                 \
   303 \          {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   304 \          : set evs;                                                  \
   305 \        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   306 \     ==> Key K ~: analz (knows Spy evs)";
   307 by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
   308 qed "B_gets_good_key";
   309 
   310 
   311 (*** Authenticating B to A: these proofs are not considered.
   312      They are irrelevant to showing the need for Oops. ***)
   313 
   314 
   315 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   316 
   317 (*Assuming the session key is secure, if both certificates are present then
   318   A has said NB.  We can't be sure about the rest of A's message, but only
   319   NB matters for freshness.*)  
   320 Goal "evs : yahalom                                              \
   321 \     ==> Key K ~: analz (knows Spy evs) -->                     \
   322 \         Crypt K (Nonce NB) : parts (knows Spy evs) -->         \
   323 \         Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs) --> \
   324 \         B ~: bad -->                                           \
   325 \         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   326 by (parts_induct_tac 1);
   327 (*Fake*)
   328 by (Fake_parts_insert_tac 1);
   329 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   330 by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
   331 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   332 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   333 (*yes: apply unicity of session keys*)
   334 by (g_not_bad_tac "Aa" 1);
   335 by (blast_tac (claset() addSEs [MPair_parts]
   336                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   337 		        addDs  [Says_imp_knows_Spy RS parts.Inj,
   338 				unique_session_keys]) 1);
   339 qed_spec_mp "A_Said_YM3_lemma";
   340 
   341 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   342   Moreover, A associates K with NB (thus is talking about the same run).
   343   Other premises guarantee secrecy of K.*)
   344 Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                   \
   345 \                 Crypt K (Nonce NB)|} : set evs;                      \
   346 \        Says B Server                                                 \
   347 \          {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   348 \          : set evs;                                                  \
   349 \        A ~: bad;  B ~: bad;  evs : yahalom |]       \
   350 \     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   351 by (ftac B_trusts_YM4 1);
   352 by (REPEAT_FIRST assume_tac);
   353 by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);
   354 by (Clarify_tac 1);
   355 by (rtac A_Said_YM3_lemma 1);
   356 by (rtac Spy_not_see_encrypted_key 2);
   357 by (REPEAT_FIRST assume_tac);
   358 qed_spec_mp "YM4_imp_A_Said_YM3";