src/HOL/Auth/WooLam.ML
author paulson
Fri Nov 29 17:58:18 1996 +0100 (1996-11-29)
changeset 2283 68829cf138fc
parent 2274 1b1b46adc9b3
child 2321 083912bc5775
permissions -rw-r--r--
Swapping arguments of Crypt; removing argument lost
     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 (*Weak liveness: 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 addss (!simpset setsolver safe_solver))));
    32 result();
    33 
    34 
    35 (**** Inductive proofs about woolam ****)
    36 
    37 (*Nobody sends themselves messages*)
    38 goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs";
    39 by (etac woolam.induct 1);
    40 by (Auto_tac());
    41 qed_spec_mp "not_Says_to_self";
    42 Addsimps [not_Says_to_self];
    43 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    44 
    45 
    46 (** For reasoning about the encrypted portion of messages **)
    47 
    48 goal thy "!!evs. Says A' B X : set_of_list evs \
    49 \                ==> X : analz (sees lost Spy evs)";
    50 by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
    51 qed "WL4_analz_sees_Spy";
    52 
    53 bind_thm ("WL4_parts_sees_Spy",
    54           WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    55 
    56 val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6;
    57 
    58 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    59 fun parts_induct_tac i = SELECT_GOAL
    60     (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
    61              (*Fake message*)
    62              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    63                                            impOfSubs Fake_parts_insert]
    64                                     addss (!simpset)) 2)) THEN
    65      (*Base case*)
    66      fast_tac (!claset addss (!simpset)) 1 THEN
    67      ALLGOALS Asm_simp_tac) i;
    68 
    69 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    70     sends messages containing X! **)
    71 
    72 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    73 goal thy 
    74  "!!evs. evs : woolam \
    75 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    76 by (parts_induct_tac 1);
    77 by (Auto_tac());
    78 qed "Spy_see_shrK";
    79 Addsimps [Spy_see_shrK];
    80 
    81 goal thy 
    82  "!!evs. evs : woolam \
    83 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    84 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    85 qed "Spy_analz_shrK";
    86 Addsimps [Spy_analz_shrK];
    87 
    88 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    89 \                  evs : woolam |] ==> A:lost";
    90 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    91 qed "Spy_see_shrK_D";
    92 
    93 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    94 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    95 
    96 
    97 (*** Future nonces can't be seen or used! ***)
    98 
    99 goal thy "!!evs. evs : woolam ==> \
   100 \                length evs <= length evt --> \
   101 \                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   102 by (parts_induct_tac 1);
   103 by (REPEAT_FIRST (fast_tac (!claset 
   104                               addSEs partsEs
   105                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
   106                               addEs [leD RS notE]
   107 			      addDs  [impOfSubs analz_subset_parts,
   108                                       impOfSubs parts_insert_subset_Un,
   109                                       Suc_leD]
   110                               addss (!simpset))));
   111 qed_spec_mp "new_nonces_not_seen";
   112 Addsimps [new_nonces_not_seen];
   113 
   114 
   115 (**** Autheticity properties for Woo-Lam ****)
   116 
   117 
   118 (*** WL4 ***)
   119 
   120 (*If the encrypted message appears then it originated with Alice*)
   121 goal thy 
   122  "!!evs. [| A ~: lost;  evs : woolam |]                   \
   123 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs)        \
   124 \        --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)";
   125 by (parts_induct_tac 1);
   126 by (Fast_tac 1);
   127 qed_spec_mp "NB_Crypt_imp_Alice_msg";
   128 
   129 (*Guarantee for Server: if it gets a message containing a certificate from 
   130   Alice, then she originated that certificate.  But we DO NOT know that B
   131   ever saw it: the Spy may have rerouted the message to the Server.*)
   132 goal thy 
   133  "!!evs. [| A ~: lost;  evs : woolam;               \
   134 \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   135 \            : set_of_list evs |]                                  \
   136 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   137 by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   138                       addSEs [MPair_parts]
   139                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   140 qed "Server_trust_WL4";
   141 
   142 
   143 (*** WL5 ***)
   144 
   145 (*Server sent WL5 only if it received the right sort of message*)
   146 goal thy 
   147  "!!evs. evs : woolam ==>                                              \
   148 \        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs   \
   149 \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   150 \               : set_of_list evs)";
   151 by (parts_induct_tac 1);
   152 by (ALLGOALS Fast_tac);
   153 bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
   154 
   155 
   156 (*If the encrypted message appears then it originated with the Server!*)
   157 goal thy 
   158  "!!evs. [| B ~: lost;  evs : woolam |]                   \
   159 \    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
   160 \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   161 by (parts_induct_tac 1);
   162 qed_spec_mp "NB_Crypt_imp_Server_msg";
   163 
   164 (*Partial guarantee for B: if it gets a message of correct form then the Server
   165   sent the same message.*)
   166 goal thy 
   167  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \
   168 \           B ~: lost;  evs : woolam |]                                  \
   169 \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs";
   170 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   171                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   172 qed "B_got_WL5";
   173 
   174 (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   175   the nonce using her key.  This event can be no older than the nonce itself.
   176   But A may have sent the nonce to some other agent and it could have reached
   177   the Server via the Spy.*)
   178 goal thy 
   179  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \
   180 \           A ~: lost;  B ~: lost;  evs : woolam  |] \
   181 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   182 by (fast_tac (!claset addIs  [Server_trust_WL4]
   183                       addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   184 qed "B_trust_WL5";
   185 
   186 
   187 (*B only issues challenges in response to WL1.  Useful??*)
   188 goal thy 
   189  "!!evs. [| B ~= Spy;  evs : woolam |]                   \
   190 \    ==> Says B A (Nonce NB) : set_of_list evs        \
   191 \        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
   192 by (parts_induct_tac 1);
   193 by (ALLGOALS Fast_tac);
   194 bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
   195 
   196 
   197 (**CANNOT be proved because A doesn't know where challenges come from...
   198 goal thy 
   199  "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
   200 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
   201 \        Says B A (Nonce NB) : set_of_list evs        \
   202 \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs";
   203 by (parts_induct_tac 1);
   204 by (Step_tac 1);
   205 by (best_tac (!claset addSEs partsEs
   206                       addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   207 **)