src/HOL/Auth/WooLam.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Auth/WooLam
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "woolam" for the Woo-Lam protocol.
     7 
     8 Simplified version from page 11 of
     9   Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    10   IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    11 *)
    12 
    13 open WooLam;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 Pretty.setdepth 20;
    18 
    19 
    20 (*A "possibility property": there are traces that reach the end*)
    21 goal thy 
    22  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    23 \        ==> EX NB. EX evs: woolam.               \
    24 \               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
    25 \                 : set_of_list evs";
    26 by (REPEAT (resolve_tac [exI,bexI] 1));
    27 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
    28           woolam.WL4 RS woolam.WL5) 2);
    29 by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
    30 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    31 by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
    32                                     addss (!simpset setSolver safe_solver))));
    33 result();
    34 
    35 
    36 (**** Inductive proofs about woolam ****)
    37 
    38 (*Nobody sends themselves messages*)
    39 goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
    40 by (etac woolam.induct 1);
    41 by (Auto_tac());
    42 qed_spec_mp "not_Says_to_self";
    43 Addsimps [not_Says_to_self];
    44 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    45 
    46 
    47 (** For reasoning about the encrypted portion of messages **)
    48 
    49 goal thy "!!evs. Says A' B X : set_of_list evs \
    50 \                ==> X : analz (sees lost Spy evs)";
    51 by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
    52 qed "WL4_analz_sees_Spy";
    53 
    54 bind_thm ("WL4_parts_sees_Spy",
    55           WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    56 
    57 val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
    58 
    59 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    60 fun parts_induct_tac i = SELECT_GOAL
    61     (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
    62              (*Fake message*)
    63              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    64                                            impOfSubs Fake_parts_insert]
    65                                     addss (!simpset)) 2)) THEN
    66      (*Base case*)
    67      fast_tac (!claset addss (!simpset)) 1 THEN
    68      ALLGOALS Asm_simp_tac) i;
    69 
    70 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    71     sends messages containing X! **)
    72 
    73 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    74 goal thy 
    75  "!!evs. evs : woolam \
    76 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    77 by (parts_induct_tac 1);
    78 by (Auto_tac());
    79 qed "Spy_see_shrK";
    80 Addsimps [Spy_see_shrK];
    81 
    82 goal thy 
    83  "!!evs. evs : woolam \
    84 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    85 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    86 qed "Spy_analz_shrK";
    87 Addsimps [Spy_analz_shrK];
    88 
    89 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    90 \                  evs : woolam |] ==> A:lost";
    91 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    92 qed "Spy_see_shrK_D";
    93 
    94 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    95 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    96 
    97 
    98 (**** Autheticity properties for Woo-Lam ****)
    99 
   100 
   101 (*** WL4 ***)
   102 
   103 (*If the encrypted message appears then it originated with Alice*)
   104 goal thy 
   105  "!!evs. [| A ~: lost;  evs : woolam |]                   \
   106 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
   107 \        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
   108 by (parts_induct_tac 1);
   109 by (Fast_tac 1);
   110 qed_spec_mp "NB_Crypt_imp_Alice_msg";
   111 
   112 (*Guarantee for Server: if it gets a message containing a certificate from 
   113   Alice, then she originated that certificate.  But we DO NOT know that B
   114   ever saw it: the Spy may have rerouted the message to the Server.*)
   115 goal thy 
   116  "!!evs. [| A ~: lost;  evs : woolam;               \
   117 \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   118 \            : set_of_list evs |]                                  \
   119 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   120 by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   121                       addSEs [MPair_parts]
   122                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   123 qed "Server_trusts_WL4";
   124 
   125 
   126 (*** WL5 ***)
   127 
   128 (*Server sent WL5 only if it received the right sort of message*)
   129 goal thy 
   130  "!!evs. evs : woolam ==>                                              \
   131 \        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
   132 \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   133 \               : set_of_list evs)";
   134 by (parts_induct_tac 1);
   135 by (ALLGOALS Fast_tac);
   136 bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
   137 
   138 
   139 (*If the encrypted message appears then it originated with the Server!*)
   140 goal thy 
   141  "!!evs. [| B ~: lost;  evs : woolam |]                   \
   142 \    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
   143 \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   144 by (parts_induct_tac 1);
   145 qed_spec_mp "NB_Crypt_imp_Server_msg";
   146 
   147 (*Partial guarantee for B: if it gets a message of correct form then the Server
   148   sent the same message.*)
   149 goal thy 
   150  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
   151 \           B ~: lost;  evs : woolam |]                                  \
   152 \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   153 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   154                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   155 qed "B_got_WL5";
   156 
   157 (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   158   the nonce using her key.  This event can be no older than the nonce itself.
   159   But A may have sent the nonce to some other agent and it could have reached
   160   the Server via the Spy.*)
   161 goal thy 
   162  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
   163 \           A ~: lost;  B ~: lost;  evs : woolam  |] \
   164 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   165 by (fast_tac (!claset addIs  [Server_trusts_WL4]
   166                       addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   167 qed "B_trusts_WL5";
   168 
   169 
   170 (*B only issues challenges in response to WL1.  Useful??*)
   171 goal thy 
   172  "!!evs. [| B ~= Spy;  evs : woolam |]                   \
   173 \    ==> Says B A (Nonce NB) : set_of_list evs        \
   174 \        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
   175 by (parts_induct_tac 1);
   176 by (ALLGOALS Fast_tac);
   177 bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
   178 
   179 
   180 (**CANNOT be proved because A doesn't know where challenges come from...
   181 goal thy 
   182  "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
   183 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
   184 \        Says B A (Nonce NB) : set_of_list evs        \
   185 \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   186 by (parts_induct_tac 1);
   187 by (Step_tac 1);
   188 by (best_tac (!claset addSEs partsEs) 1);
   189 **)