src/HOL/Auth/KerberosIV.ML
changeset 11104 f2024fed9f0c
parent 10833 c0844a30ea4e
child 11185 1b737b4c2108
equal deleted inserted replaced
11103:2a3cc8e1723a 11104:f2024fed9f0c
   356 \     ==> ServKey ~: range shrK & \
   356 \     ==> ServKey ~: range shrK & \
   357 \         (EX A. ServTicket = \
   357 \         (EX A. ServTicket = \
   358 \                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})  \
   358 \                 Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})  \
   359 \          | ServTicket : analz (spies evs)";
   359 \          | ServTicket : analz (spies evs)";
   360 by (case_tac "Key AuthKey : analz (spies evs)" 1);
   360 by (case_tac "Key AuthKey : analz (spies evs)" 1);
   361 by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);
   361 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1); 
   362 by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   362 by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   363 by (blast_tac (claset() addSDs [ServTicket_form]) 1);
   363 by (blast_tac (claset() addSDs [ServTicket_form]) 1);
   364 qed "Says_tgs_message_form";
   364 qed "Says_tgs_message_form";
   365 (* This form MUST be used in analz_sees_tac below *)
   365 (* This form MUST be used in analz_sees_tac below *)
   366 
   366 
   368 (*****************UNICITY THEOREMS****************)
   368 (*****************UNICITY THEOREMS****************)
   369 
   369 
   370 (* The session key, if secure, uniquely identifies the Ticket
   370 (* The session key, if secure, uniquely identifies the Ticket
   371    whether AuthTicket or ServTicket. As a matter of fact, one can read
   371    whether AuthTicket or ServTicket. As a matter of fact, one can read
   372    also Tgs in the place of B.                                     *)
   372    also Tgs in the place of B.                                     *)
   373 Goal "evs : kerberos ==>                                        \
       
   374 \     Key SesKey ~: analz (spies evs) -->   \
       
   375 \     (EX A B T. ALL A' B' T'.                          \
       
   376 \      Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}    \
       
   377 \        : parts (spies evs) --> A'=A & B'=B & T'=T)";
       
   378 by (parts_induct_tac 1);
       
   379 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
       
   380     THEN Fake_parts_insert_tac 1);
       
   381 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
       
   382 by (expand_case_tac "SesKey = ?y" 1);
       
   383 by (blast_tac (claset() addSEs spies_partsEs) 1);
       
   384 by (expand_case_tac "SesKey = ?y" 1);
       
   385 by (blast_tac (claset() addSEs spies_partsEs) 1);
       
   386 val lemma = result();
       
   387 
   373 
   388 Goal "[| Crypt (shrK B)  {|Agent A,  Agent B,  Key SesKey, T|}        \
   374 Goal "[| Crypt (shrK B)  {|Agent A,  Agent B,  Key SesKey, T|}        \
   389 \          : parts (spies evs);            \
   375 \          : parts (spies evs);            \
   390 \        Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}     \
   376 \        Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}     \
   391 \          : parts (spies evs);            \
   377 \          : parts (spies evs);  Key SesKey ~: analz (spies evs);   \
   392 \        evs : kerberos;  Key SesKey ~: analz (spies evs) |]  \
   378 \        evs : kerberos |]  \
   393 \     ==> A=A' & B=B' & T=T'";
   379 \     ==> A=A' & B=B' & T=T'";
   394 by (prove_unique_tac lemma 1);
   380 by (etac rev_mp 1);
       
   381 by (etac rev_mp 1);
       
   382 by (etac rev_mp 1);
       
   383 by (parts_induct_tac 1);
       
   384 (*Fake, K2, K4*)
       
   385 by (Fake_parts_insert_tac 1);
       
   386 by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
   395 qed "unique_CryptKey";
   387 qed "unique_CryptKey";
   396 
       
   397 Goal "evs : kerberos \
       
   398 \     ==> Key SesKey ~: analz (spies evs) -->   \
       
   399 \         (EX K' B' T' Ticket'. ALL K B T Ticket.                          \
       
   400 \          Crypt K {|Key SesKey, Agent B, T, Ticket|}    \
       
   401 \            : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
       
   402 by (parts_induct_tac 1);
       
   403 by (REPEAT (etac (exI RSN (2,exE)) 1) THEN Fake_parts_insert_tac 1);
       
   404 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
       
   405 by (expand_case_tac "SesKey = ?y" 1);
       
   406 by (blast_tac (claset() addSEs spies_partsEs) 1);
       
   407 by (expand_case_tac "SesKey = ?y" 1);
       
   408 by (blast_tac (claset() addSEs spies_partsEs) 1);
       
   409 val lemma = result();
       
   410 
   388 
   411 (*An AuthKey is encrypted by one and only one Shared key.
   389 (*An AuthKey is encrypted by one and only one Shared key.
   412   A ServKey is encrypted by one and only one AuthKey.
   390   A ServKey is encrypted by one and only one AuthKey.
   413 *)
   391 *)
   414 Goal "[| Crypt K  {|Key SesKey,  Agent B, T, Ticket|}        \
   392 Goal "[| Crypt K  {|Key SesKey,  Agent B, T, Ticket|}        \
   415 \          : parts (spies evs);            \
   393 \          : parts (spies evs);            \
   416 \        Crypt K' {|Key SesKey,  Agent B', T', Ticket'|}     \
   394 \        Crypt K' {|Key SesKey,  Agent B', T', Ticket'|}     \
   417 \          : parts (spies evs);            \
   395 \          : parts (spies evs);  Key SesKey ~: analz (spies evs);            \
   418 \        evs : kerberos;  Key SesKey ~: analz (spies evs) |]  \
   396 \        evs : kerberos |]  \
   419 \     ==> K=K' & B=B' & T=T' & Ticket=Ticket'";
   397 \     ==> K=K' & B=B' & T=T' & Ticket=Ticket'";
   420 by (prove_unique_tac lemma 1);
   398 by (etac rev_mp 1);
       
   399 by (etac rev_mp 1);
       
   400 by (etac rev_mp 1);
       
   401 by (parts_induct_tac 1);
       
   402 (*Fake, K2, K4*)
       
   403 by (Fake_parts_insert_tac 1);
       
   404 by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 
   421 qed "Key_unique_SesKey";
   405 qed "Key_unique_SesKey";
   422 
   406 
   423 
   407 
   424 (*
   408 (*
   425   At reception of any message mentioning A, Kas associates shrK A with
   409   At reception of any message mentioning A, Kas associates shrK A with
   437   \          : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
   421   \          : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
   438 
   422 
   439   would fail on the K2 and K4 cases.
   423   would fail on the K2 and K4 cases.
   440 *)
   424 *)
   441 
   425 
   442 (* AuthKey uniquely identifies the message from Kas *)
       
   443 Goal "evs : kerberos ==>                                        \
       
   444 \      EX A' Ka' Tk' X'. ALL A Ka Tk X.                          \
       
   445 \        Says Kas A (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|})  \
       
   446 \          : set evs --> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
       
   447 by (etac kerberos.induct 1);
       
   448 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
       
   449 by (Step_tac 1);
       
   450 (*K2: it can't be a new key*)
       
   451 by (expand_case_tac "AuthKey = ?y" 1);
       
   452 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
       
   453 by (blast_tac (claset() delrules [conjI]   (*prevent split-up into 4 subgoals*)
       
   454                       addSEs spies_partsEs) 1);
       
   455 val lemma = result();
       
   456 
       
   457 Goal "[| Says Kas A                                          \
   426 Goal "[| Says Kas A                                          \
   458 \             (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) : set evs;     \ 
   427 \             (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) : set evs;     \ 
   459 \        Says Kas A'                                         \
   428 \        Says Kas A'                                         \
   460 \             (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) : set evs;   \
   429 \             (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) : set evs;   \
   461 \        evs : kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
   430 \        evs : kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
   462 by (prove_unique_tac lemma 1);
   431 by (etac rev_mp 1);
       
   432 by (etac rev_mp 1);
       
   433 by (parts_induct_tac 1);
       
   434 (*K2*)
       
   435 by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
   463 qed "unique_AuthKeys";
   436 qed "unique_AuthKeys";
   464 
   437 
   465 (* ServKey uniquely identifies the message from Tgs *)
   438 (* ServKey uniquely identifies the message from Tgs *)
   466 Goal "evs : kerberos ==>                                        \
       
   467 \      EX A' B' AuthKey' Tk' X'. ALL A B AuthKey Tk X.                     \
       
   468 \        Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tk, X|})  \
       
   469 \          : set evs --> A=A' & B=B' & AuthKey=AuthKey' & Tk=Tk' & X=X'";
       
   470 by (etac kerberos.induct 1);
       
   471 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
       
   472 by (Step_tac 1);
       
   473 (*K4: it can't be a new key*)
       
   474 by (expand_case_tac "ServKey = ?y" 1);
       
   475 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
       
   476 by (blast_tac (claset() delrules [conjI]   (*prevent split-up into 4 subgoals*)
       
   477                       addSEs spies_partsEs) 1);
       
   478 val lemma = result();
       
   479 
       
   480 Goal "[| Says Tgs A                                             \
   439 Goal "[| Says Tgs A                                             \
   481 \             (Crypt K {|Key ServKey, Agent B, Tt, X|}) : set evs; \ 
   440 \             (Crypt K {|Key ServKey, Agent B, Tt, X|}) : set evs; \ 
   482 \        Says Tgs A'                                                 \
   441 \        Says Tgs A'                                                 \
   483 \             (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) : set evs; \
   442 \             (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) : set evs; \
   484 \        evs : kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
   443 \        evs : kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
   485 by (prove_unique_tac lemma 1);
   444 by (etac rev_mp 1);
       
   445 by (etac rev_mp 1);
       
   446 by (parts_induct_tac 1);
       
   447 (*K4*)
       
   448 by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
   486 qed "unique_ServKeys";
   449 qed "unique_ServKeys";
   487 
   450 
   488 
   451 
   489 (*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
   452 (*****************LEMMAS ABOUT the predicate KeyCryptKey****************)
   490 
   453