src/HOL/Auth/Yahalom.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
equal deleted inserted replaced
4536:74f7c556fd90 4537:4e835bd9fada
   200 
   200 
   201 
   201 
   202 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   202 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   203 
   203 
   204 goal thy 
   204 goal thy 
   205  "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]         \
   205  "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]                \
   206 \        ==> Says Server A                                        \
   206 \        ==> Says Server A                                        \
   207 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   207 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   208 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   208 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   209 \             : set evs -->                                       \
   209 \             : set evs -->                                       \
   210 \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
   210 \            Notes Spy {|na, nb, Key K|} ~: set evs -->           \
   211 \            Key K ~: analz (spies evs)";
   211 \            Key K ~: analz (spies evs)";
   212 by (etac yahalom.induct 1);
   212 by (etac yahalom.induct 1);
   213 by analz_spies_tac;
   213 by analz_spies_tac;
   214 by (ALLGOALS
   214 by (ALLGOALS
   215     (asm_simp_tac 
   215     (asm_simp_tac 
   230 goal thy 
   230 goal thy 
   231  "!!evs. [| Says Server A                                         \
   231  "!!evs. [| Says Server A                                         \
   232 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   232 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   233 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   233 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   234 \             : set evs;                                          \
   234 \             : set evs;                                          \
   235 \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   235 \           Notes Spy {|na, nb, Key K|} ~: set evs;               \
   236 \           A ~: bad;  B ~: bad;  evs : yahalom |]         \
   236 \           A ~: bad;  B ~: bad;  evs : yahalom |]                \
   237 \        ==> Key K ~: analz (spies evs)";
   237 \        ==> Key K ~: analz (spies evs)";
   238 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   238 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   239 by (blast_tac (claset() addSEs [lemma]) 1);
   239 by (blast_tac (claset() addSEs [lemma]) 1);
   240 qed "Spy_not_see_encrypted_key";
   240 qed "Spy_not_see_encrypted_key";
   241 
   241 
   320 by (Simp_tac 1);
   320 by (Simp_tac 1);
   321 by (Blast_tac 1);
   321 by (Blast_tac 1);
   322 qed "KeyWithNonce_Says";
   322 qed "KeyWithNonce_Says";
   323 Addsimps [KeyWithNonce_Says];
   323 Addsimps [KeyWithNonce_Says];
   324 
   324 
       
   325 goalw thy [KeyWithNonce_def]
       
   326    "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
       
   327 by (Simp_tac 1);
       
   328 qed "KeyWithNonce_Notes";
       
   329 Addsimps [KeyWithNonce_Notes];
       
   330 
   325 (*A fresh key cannot be associated with any nonce 
   331 (*A fresh key cannot be associated with any nonce 
   326   (with respect to a given trace). *)
   332   (with respect to a given trace). *)
   327 goalw thy [KeyWithNonce_def]
   333 goalw thy [KeyWithNonce_def]
   328  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   334  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   329 by (blast_tac (claset() addSEs spies_partsEs) 1);
   335 by (blast_tac (claset() addSEs spies_partsEs) 1);
   370 by (ALLGOALS  (*12 seconds*)
   376 by (ALLGOALS  (*12 seconds*)
   371     (asm_simp_tac 
   377     (asm_simp_tac 
   372      (analz_image_freshK_ss 
   378      (analz_image_freshK_ss 
   373        addsimps expand_ifs
   379        addsimps expand_ifs
   374        addsimps [all_conj_distrib, analz_image_freshK,
   380        addsimps [all_conj_distrib, analz_image_freshK,
   375 		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
   381 		 KeyWithNonce_Says, KeyWithNonce_Notes,
       
   382 		 fresh_not_KeyWithNonce, 
   376 		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
   383 		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
   377 		 Says_Server_KeyWithNonce])));
   384 		 Says_Server_KeyWithNonce])));
   378 (*Fake*) 
   385 (*Fake*) 
   379 by (spy_analz_tac 1);
   386 by (spy_analz_tac 1);
   380 (*YM4*)  (** LEVEL 6 **)
   387 (*YM4*)  (** LEVEL 6 **)
   476 goal thy 
   483 goal thy 
   477  "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]  \
   484  "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]  \
   478 \ ==> Says B Server                                                    \
   485 \ ==> Says B Server                                                    \
   479 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   486 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   480 \     : set evs -->                                                    \
   487 \     : set evs -->                                                    \
   481 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   488 \     (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->      \
   482 \     Nonce NB ~: analz (spies evs)";
   489 \     Nonce NB ~: analz (spies evs)";
   483 by (etac yahalom.induct 1);
   490 by (etac yahalom.induct 1);
   484 by analz_spies_tac;
   491 by analz_spies_tac;
   485 by (ALLGOALS
   492 by (ALLGOALS
   486     (asm_simp_tac 
   493     (asm_simp_tac 
   527 			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   534 			        no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   528 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   535 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   529 
   536 
   530 
   537 
   531 (*B's session key guarantee from YM4.  The two certificates contribute to a
   538 (*B's session key guarantee from YM4.  The two certificates contribute to a
   532   single conclusion about the Server's message.  Note that the "Says A Spy"
   539   single conclusion about the Server's message.  Note that the "Notes Spy"
   533   assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   540   assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   534   If this run is broken and the spy substitutes a certificate containing an
   541   If this run is broken and the spy substitutes a certificate containing an
   535   old key, B has no means of telling.*)
   542   old key, B has no means of telling.*)
   536 goal thy 
   543 goal thy 
   537  "!!evs. [| Says B Server                                                   \
   544  "!!evs. [| Says B Server                                                   \
   538 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   545 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   539 \             : set evs;                                                    \
   546 \             : set evs;                                                    \
   540 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   547 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   541 \                       Crypt K (Nonce NB)|} : set evs;                     \
   548 \                       Crypt K (Nonce NB)|} : set evs;                     \
   542 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   549 \           ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
   543 \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   550 \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   544 \         ==> Says Server A                                                 \
   551 \         ==> Says Server A                                                 \
   545 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   552 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   546 \                               Nonce NA, Nonce NB|},                       \
   553 \                               Nonce NA, Nonce NB|},                       \
   547 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   554 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   634  "!!evs. [| Says B Server                                                   \
   641  "!!evs. [| Says B Server                                                   \
   635 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   642 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   636 \             : set evs;                                                    \
   643 \             : set evs;                                                    \
   637 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   644 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   638 \                       Crypt K (Nonce NB)|} : set evs;                     \
   645 \                       Crypt K (Nonce NB)|} : set evs;                     \
   639 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   646 \           (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs);     \
   640 \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   647 \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   641 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   648 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   642 by (dtac B_trusts_YM4 1);
   649 by (dtac B_trusts_YM4 1);
   643 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   650 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   644 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   651 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);