Addition of Woo-Lam protocol
authorpaulson
Thu Nov 28 15:56:04 1996 +0100 (1996-11-28)
changeset 22741b1b46adc9b3
parent 2273 d1bcc10be8d7
child 2275 dbce3dce821a
Addition of Woo-Lam protocol
src/HOL/Auth/ROOT.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
src/HOL/Makefile
     1.1 --- a/src/HOL/Auth/ROOT.ML	Thu Nov 28 12:47:48 1996 +0100
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Thu Nov 28 15:56:04 1996 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4  use_thy "OtwayRees";
     1.5  use_thy "OtwayRees_AN";
     1.6  use_thy "OtwayRees_Bad";
     1.7 +use_thy "WooLam";
     1.8  use_thy "Yahalom";
     1.9  use_thy "Yahalom2";
    1.10  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/WooLam.ML	Thu Nov 28 15:56:04 1996 +0100
     2.3 @@ -0,0 +1,209 @@
     2.4 +(*  Title:      HOL/Auth/WooLam
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Inductive relation "woolam" for the Woo-Lam protocol.
    2.10 +
    2.11 +Simplified version from page 11 of
    2.12 +  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    2.13 +  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    2.14 +*)
    2.15 +
    2.16 +open WooLam;
    2.17 +
    2.18 +proof_timing:=true;
    2.19 +HOL_quantifiers := false;
    2.20 +Pretty.setdepth 20;
    2.21 +
    2.22 +
    2.23 +(*Weak liveness: there are traces that reach the end*)
    2.24 +goal thy 
    2.25 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    2.26 +\        ==> EX NB. EX evs: woolam lost.          \
    2.27 +\               Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) \
    2.28 +\                 : set_of_list evs";
    2.29 +by (REPEAT (resolve_tac [exI,bexI] 1));
    2.30 +by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
    2.31 +	  woolam.WL4 RS woolam.WL5) 2);
    2.32 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    2.33 +by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    2.34 +by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    2.35 +result();
    2.36 +
    2.37 +
    2.38 +(**** Inductive proofs about woolam ****)
    2.39 +
    2.40 +(*Nobody sends themselves messages*)
    2.41 +goal thy "!!evs. evs : woolam lost ==> ALL A X. Says A A X ~: set_of_list evs";
    2.42 +by (etac woolam.induct 1);
    2.43 +by (Auto_tac());
    2.44 +qed_spec_mp "not_Says_to_self";
    2.45 +Addsimps [not_Says_to_self];
    2.46 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    2.47 +
    2.48 +
    2.49 +(** For reasoning about the encrypted portion of messages **)
    2.50 +
    2.51 +goal thy "!!evs. Says A' B X : set_of_list evs \
    2.52 +\                ==> X : analz (sees lost Spy evs)";
    2.53 +by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
    2.54 +qed "WL4_analz_sees_Spy";
    2.55 +
    2.56 +bind_thm ("WL4_parts_sees_Spy",
    2.57 +          WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    2.58 +
    2.59 +(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    2.60 +  harder to complete, since simplification does less for us.*)
    2.61 +val parts_Fake_tac = forw_inst_tac [("lost","lost")] WL4_parts_sees_Spy 6;
    2.62 +
    2.63 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    2.64 +fun parts_induct_tac i = SELECT_GOAL
    2.65 +    (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN
    2.66 +             (*Fake message*)
    2.67 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    2.68 +                                           impOfSubs Fake_parts_insert]
    2.69 +                                    addss (!simpset)) 2)) THEN
    2.70 +     (*Base case*)
    2.71 +     fast_tac (!claset addss (!simpset)) 1 THEN
    2.72 +     ALLGOALS Asm_simp_tac) i;
    2.73 +
    2.74 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    2.75 +    sends messages containing X! **)
    2.76 +
    2.77 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    2.78 +goal thy 
    2.79 + "!!evs. evs : woolam lost \
    2.80 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    2.81 +by (parts_induct_tac 1);
    2.82 +by (Auto_tac());
    2.83 +qed "Spy_see_shrK";
    2.84 +Addsimps [Spy_see_shrK];
    2.85 +
    2.86 +goal thy 
    2.87 + "!!evs. evs : woolam lost \
    2.88 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    2.89 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    2.90 +qed "Spy_analz_shrK";
    2.91 +Addsimps [Spy_analz_shrK];
    2.92 +
    2.93 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    2.94 +\                  evs : woolam lost |] ==> A:lost";
    2.95 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    2.96 +qed "Spy_see_shrK_D";
    2.97 +
    2.98 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    2.99 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   2.100 +
   2.101 +
   2.102 +(*** Future nonces can't be seen or used! ***)
   2.103 +
   2.104 +goal thy "!!evs. evs : woolam lost ==> \
   2.105 +\                length evs <= length evt --> \
   2.106 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   2.107 +by (parts_induct_tac 1);
   2.108 +by (REPEAT_FIRST (fast_tac (!claset 
   2.109 +                              addSEs partsEs
   2.110 +                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   2.111 +                              addEs [leD RS notE]
   2.112 +			      addDs  [impOfSubs analz_subset_parts,
   2.113 +                                      impOfSubs parts_insert_subset_Un,
   2.114 +                                      Suc_leD]
   2.115 +                              addss (!simpset))));
   2.116 +qed_spec_mp "new_nonces_not_seen";
   2.117 +Addsimps [new_nonces_not_seen];
   2.118 +
   2.119 +
   2.120 +(**** Autheticity properties for Woo-Lam ****)
   2.121 +
   2.122 +
   2.123 +(*** WL4 ***)
   2.124 +
   2.125 +(*If the encrypted message appears then it originated with Alice*)
   2.126 +goal thy 
   2.127 + "!!evs. [| A ~: lost;  evs : woolam lost |]                   \
   2.128 +\    ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs)        \
   2.129 +\        --> (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)";
   2.130 +by (parts_induct_tac 1);
   2.131 +by (Fast_tac 1);
   2.132 +qed_spec_mp "NB_Crypt_imp_Alice_msg";
   2.133 +
   2.134 +(*Guarantee for Server: if it gets a message containing a certificate from 
   2.135 +  Alice, then she originated that certificate.  But we DO NOT know that B
   2.136 +  ever saw it: the Spy may have rerouted the message to the Server.*)
   2.137 +goal thy 
   2.138 + "!!evs. [| A ~: lost;  evs : woolam lost;               \
   2.139 +\           Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} \
   2.140 +\            : set_of_list evs |]                                  \
   2.141 +\        ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
   2.142 +by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   2.143 +                      addSEs [MPair_parts]
   2.144 +                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   2.145 +qed "Server_trust_WL4";
   2.146 +
   2.147 +
   2.148 +(*** WL5 ***)
   2.149 +
   2.150 +(*Server sent WL5 only if it received the right sort of message*)
   2.151 +goal thy 
   2.152 + "!!evs. evs : woolam lost ==>                                              \
   2.153 +\        Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs   \
   2.154 +\        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt NB (shrK A)|} \
   2.155 +\               : set_of_list evs)";
   2.156 +by (parts_induct_tac 1);
   2.157 +by (ALLGOALS Fast_tac);
   2.158 +bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp));
   2.159 +
   2.160 +
   2.161 +(*If the encrypted message appears then it originated with the Server!*)
   2.162 +goal thy 
   2.163 + "!!evs. [| B ~: lost;  evs : woolam lost |]                   \
   2.164 +\    ==> Crypt {|Agent A, NB|} (shrK B) : parts (sees lost Spy evs)        \
   2.165 +\        --> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
   2.166 +by (parts_induct_tac 1);
   2.167 +qed_spec_mp "NB_Crypt_imp_Server_msg";
   2.168 +
   2.169 +(*Partial guarantee for B: if it gets a message of correct form then the Server
   2.170 +  sent the same message.*)
   2.171 +goal thy 
   2.172 + "!!evs. [| Says S B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs; \
   2.173 +\           B ~: lost;  evs : woolam lost |]                                  \
   2.174 +\        ==> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs";
   2.175 +by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   2.176 +                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   2.177 +qed "B_got_WL5";
   2.178 +
   2.179 +(*Guarantee for B.  If B gets the Server's certificate then A has encrypted
   2.180 +  the nonce using her key.  This event can be no older than the nonce itself.
   2.181 +  But A may have sent the nonce to some other agent and it could have reached
   2.182 +  the Server via the Spy.*)
   2.183 +goal thy 
   2.184 + "!!evs. [| Says S B (Crypt {|Agent A, Nonce NB|} (shrK B)): set_of_list evs; \
   2.185 +\           A ~: lost;  B ~: lost;  evs : woolam lost  |] \
   2.186 +\        ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
   2.187 +by (fast_tac (!claset addIs  [Server_trust_WL4]
   2.188 +                      addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   2.189 +qed "B_trust_WL5";
   2.190 +
   2.191 +
   2.192 +(*B only issues challenges in response to WL1.  Useful??*)
   2.193 +goal thy 
   2.194 + "!!evs. [| B ~= Spy;  evs : woolam lost |]                   \
   2.195 +\    ==> Says B A (Nonce NB) : set_of_list evs        \
   2.196 +\        --> (EX A'. Says A' B (Agent A) : set_of_list evs)";
   2.197 +by (parts_induct_tac 1);
   2.198 +by (ALLGOALS Fast_tac);
   2.199 +bind_thm ("B_said_WL2", result() RSN (2, rev_mp));
   2.200 +
   2.201 +
   2.202 +(**CANNOT be proved because A doesn't know where challenges come from...
   2.203 +goal thy 
   2.204 + "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam lost |]                   \
   2.205 +\    ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) &  \
   2.206 +\        Says B A (Nonce NB) : set_of_list evs        \
   2.207 +\        --> Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs";
   2.208 +by (parts_induct_tac 1);
   2.209 +by (Step_tac 1);
   2.210 +by (best_tac (!claset addSEs partsEs
   2.211 +                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   2.212 +**)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Nov 28 15:56:04 1996 +0100
     3.3 @@ -0,0 +1,62 @@
     3.4 +(*  Title:      HOL/Auth/WooLam
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1996  University of Cambridge
     3.8 +
     3.9 +Inductive relation "woolam" for the Woo-Lam protocol.
    3.10 +
    3.11 +Simplified version from page 11 of
    3.12 +  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    3.13 +  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    3.14 +
    3.15 +Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
    3.16 +  Some New Attacks upon Security Protocols.
    3.17 +  Computer Security Foundations Workshop, 1996.
    3.18 +*)
    3.19 +
    3.20 +WooLam = Shared + 
    3.21 +
    3.22 +consts  woolam   :: "agent set => event list set"
    3.23 +inductive "woolam lost"
    3.24 +  intrs 
    3.25 +         (*Initial trace is empty*)
    3.26 +    Nil  "[]: woolam lost"
    3.27 +
    3.28 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    3.29 +           invent new nonces here, but he can also use NS1.  Common to
    3.30 +           all similar protocols.*)
    3.31 +    Fake "[| evs: woolam lost;  B ~= Spy;  
    3.32 +             X: synth (analz (sees lost Spy evs)) |]
    3.33 +          ==> Says Spy B X  # evs : woolam lost"
    3.34 +
    3.35 +         (*Alice initiates a protocol run*)
    3.36 +    WL1  "[| evs: woolam lost;  A ~= B |]
    3.37 +          ==> Says A B (Agent A) # evs : woolam lost"
    3.38 +
    3.39 +         (*Bob responds to Alice's message with a challenge.*)
    3.40 +    WL2  "[| evs: woolam lost;  A ~= B;
    3.41 +             Says A' B (Agent A) : set_of_list evs |]
    3.42 +          ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
    3.43 +
    3.44 +         (*Alice responds to Bob's challenge by encrypting NB with her key.
    3.45 +           B is *not* properly determined -- Alice essentially broadcasts
    3.46 +           her reply.*)
    3.47 +    WL3  "[| evs: woolam lost;  A ~= B;
    3.48 +             Says B' A (Nonce NB) : set_of_list evs;
    3.49 +             Says A  B (Agent A)  : set_of_list evs |]
    3.50 +          ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
    3.51 +
    3.52 +         (*Bob forwards Alice's response to the Server.*)
    3.53 +    WL4  "[| evs: woolam lost;  B ~= Server;  
    3.54 +             Says A'  B X         : set_of_list evs;
    3.55 +             Says A'' B (Agent A) : set_of_list evs |]
    3.56 +          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
    3.57 +
    3.58 +         (*Server decrypts Alice's response for Bob.*)
    3.59 +    WL5  "[| evs: woolam lost;  B ~= Server;
    3.60 +             Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
    3.61 +               : set_of_list evs |]
    3.62 +          ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
    3.63 +                 # evs : woolam lost"
    3.64 +
    3.65 +end
     4.1 --- a/src/HOL/Makefile	Thu Nov 28 12:47:48 1996 +0100
     4.2 +++ b/src/HOL/Makefile	Thu Nov 28 15:56:04 1996 +0100
     4.3 @@ -136,7 +136,7 @@
     4.4  
     4.5  ##Authentication & Security Protocols
     4.6  Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
     4.7 -	     Yahalom Yahalom2
     4.8 +	     WooLam Yahalom Yahalom2
     4.9  
    4.10  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    4.11