added new theory Yahalom_Bad
authorpaulson
Thu Mar 18 10:41:33 1999 +0100 (1999-03-18)
changeset 64001f495d4d922b
parent 6399 4a9040b85e2e
child 6401 2462d0c077b5
added new theory Yahalom_Bad
src/HOL/Auth/README.html
src/HOL/Auth/ROOT.ML
src/HOL/Auth/Yahalom_Bad.ML
src/HOL/Auth/Yahalom_Bad.thy
     1.1 --- a/src/HOL/Auth/README.html	Thu Mar 18 10:41:00 1999 +0100
     1.2 +++ b/src/HOL/Auth/README.html	Thu Mar 18 10:41:33 1999 +0100
     1.3 @@ -14,7 +14,10 @@
     1.4  
     1.5  <LI>the Needham-Schroeder protocol (public-key and shared-key versions)
     1.6  
     1.7 -<LI>two versions of the Yahalom protocol
     1.8 +<LI>the Kerberos protocol (the simplified form published in the BAN paper)
     1.9 +
    1.10 +<LI>three versions of the Yahalom protocol, including a bad one that 
    1.11 +	illustrates the purpose of the Oops rule
    1.12  
    1.13  <LI>a novel recursive authentication protocol 
    1.14  
     2.1 --- a/src/HOL/Auth/ROOT.ML	Thu Mar 18 10:41:00 1999 +0100
     2.2 +++ b/src/HOL/Auth/ROOT.ML	Thu Mar 18 10:41:33 1999 +0100
     2.3 @@ -22,6 +22,7 @@
     2.4  time_use_thy "Recur";
     2.5  time_use_thy "Yahalom";
     2.6  time_use_thy "Yahalom2";
     2.7 +time_use_thy "Yahalom_Bad";
     2.8  
     2.9  (*Public-key protocols*)
    2.10  time_use_thy "NS_Public_Bad";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/Yahalom_Bad.ML	Thu Mar 18 10:41:33 1999 +0100
     3.3 @@ -0,0 +1,358 @@
     3.4 +(*  Title:      HOL/Auth/Yahalom
     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 "yahalom" for the Yahalom protocol.
    3.10 +
    3.11 +From page 257 of
    3.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    3.13 +  Proc. Royal Soc. 426 (1989)
    3.14 +*)
    3.15 +
    3.16 +(*A "possibility property": there are traces that reach the end*)
    3.17 +Goal "A ~= Server \
    3.18 +\     ==> EX X NB K. EX evs: yahalom.          \
    3.19 +\            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    3.20 +by (REPEAT (resolve_tac [exI,bexI] 1));
    3.21 +by (rtac (yahalom.Nil RS 
    3.22 +          yahalom.YM1 RS yahalom.Reception RS
    3.23 +          yahalom.YM2 RS yahalom.Reception RS 
    3.24 +          yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
    3.25 +by possibility_tac;
    3.26 +result();
    3.27 +
    3.28 +Goal "[| Gets B X : set evs; evs : yahalom |] ==> EX A. Says A B X : set evs";
    3.29 +by (etac rev_mp 1);
    3.30 +by (etac yahalom.induct 1);
    3.31 +by Auto_tac;
    3.32 +qed "Gets_imp_Says";
    3.33 +
    3.34 +(*Must be proved separately for each protocol*)
    3.35 +Goal "[| Gets B X : set evs; evs : yahalom |]  ==> X : knows Spy evs";
    3.36 +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
    3.37 +qed"Gets_imp_knows_Spy";
    3.38 +AddDs [Gets_imp_knows_Spy RS parts.Inj];
    3.39 +
    3.40 +fun g_not_bad_tac s = 
    3.41 +  forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s;
    3.42 +
    3.43 +
    3.44 +(**** Inductive proofs about yahalom ****)
    3.45 +
    3.46 +
    3.47 +(** For reasoning about the encrypted portion of messages **)
    3.48 +
    3.49 +(*Lets us treat YM4 using a similar argument as for the Fake case.*)
    3.50 +Goal "[| Gets A {|Crypt (shrK A) Y, X|} : set evs;  evs : yahalom |]  \
    3.51 +\     ==> X : analz (knows Spy evs)";
    3.52 +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
    3.53 +qed "YM4_analz_knows_Spy";
    3.54 +
    3.55 +bind_thm ("YM4_parts_knows_Spy",
    3.56 +          YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
    3.57 +
    3.58 +(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
    3.59 +fun parts_knows_Spy_tac i = 
    3.60 +  EVERY
    3.61 +   [forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6),
    3.62 +    prove_simple_subgoals_tac i];
    3.63 +
    3.64 +(*Induction for regularity theorems.  If induction formula has the form
    3.65 +   X ~: analz (knows Spy evs) --> ... then it shortens the proof by discarding
    3.66 +   needless information about analz (insert X (knows Spy evs))  *)
    3.67 +fun parts_induct_tac i = 
    3.68 +    etac yahalom.induct i
    3.69 +    THEN 
    3.70 +    REPEAT (FIRSTGOAL analz_mono_contra_tac)
    3.71 +    THEN  parts_knows_Spy_tac i;
    3.72 +
    3.73 +
    3.74 +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
    3.75 +    sends messages containing X! **)
    3.76 +
    3.77 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    3.78 +Goal "evs : yahalom ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
    3.79 +by (parts_induct_tac 1);
    3.80 +by (Fake_parts_insert_tac 1);
    3.81 +by (ALLGOALS Blast_tac);
    3.82 +qed "Spy_see_shrK";
    3.83 +Addsimps [Spy_see_shrK];
    3.84 +
    3.85 +Goal "evs : yahalom ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
    3.86 +by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    3.87 +qed "Spy_analz_shrK";
    3.88 +Addsimps [Spy_analz_shrK];
    3.89 +
    3.90 +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    3.91 +	Spy_analz_shrK RSN (2, rev_iffD1)];
    3.92 +
    3.93 +
    3.94 +(*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
    3.95 +Goal "evs : yahalom ==>          \
    3.96 +\      Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
    3.97 +by (parts_induct_tac 1);
    3.98 +(*Fake*)
    3.99 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   3.100 +(*YM2-4: Because Key K is not fresh, etc.*)
   3.101 +by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
   3.102 +qed_spec_mp "new_keys_not_used";
   3.103 +
   3.104 +bind_thm ("new_keys_not_analzd",
   3.105 +          [analz_subset_parts RS keysFor_mono,
   3.106 +           new_keys_not_used] MRS contra_subsetD);
   3.107 +
   3.108 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   3.109 +
   3.110 +
   3.111 +(*For proofs involving analz.*)
   3.112 +val analz_knows_Spy_tac = 
   3.113 +    forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7;
   3.114 +
   3.115 +(****
   3.116 + The following is to prove theorems of the form
   3.117 +
   3.118 +  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
   3.119 +  Key K : analz (knows Spy evs)
   3.120 +
   3.121 + A more general formula must be proved inductively.
   3.122 +****)
   3.123 +
   3.124 +(** Session keys are not used to encrypt other session keys **)
   3.125 +
   3.126 +Goal "evs : yahalom ==>                              \
   3.127 +\  ALL K KK. KK <= - (range shrK) -->                \
   3.128 +\         (Key K : analz (Key``KK Un (knows Spy evs))) = \
   3.129 +\         (K : KK | Key K : analz (knows Spy evs))";
   3.130 +by (etac yahalom.induct 1);
   3.131 +by analz_knows_Spy_tac;
   3.132 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   3.133 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   3.134 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   3.135 +(*Fake*) 
   3.136 +by (spy_analz_tac 1);
   3.137 +qed_spec_mp "analz_image_freshK";
   3.138 +
   3.139 +Goal "[| evs : yahalom;  KAB ~: range shrK |]                  \
   3.140 +\      ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
   3.141 +\          (K = KAB | Key K : analz (knows Spy evs))";
   3.142 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   3.143 +qed "analz_insert_freshK";
   3.144 +
   3.145 +
   3.146 +(*** The Key K uniquely identifies the Server's  message. **)
   3.147 +
   3.148 +Goal "evs : yahalom ==>                                     \
   3.149 +\   EX A' B' na' nb' X'. ALL A B na nb X.                   \
   3.150 +\       Says Server A                                       \
   3.151 +\        {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}   \
   3.152 +\       : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   3.153 +by (etac yahalom.induct 1);
   3.154 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   3.155 +by (ALLGOALS Clarify_tac);
   3.156 +by (ex_strip_tac 2);
   3.157 +by (Blast_tac 2);
   3.158 +(*Remaining case: YM3*)
   3.159 +by (expand_case_tac "K = ?y" 1);
   3.160 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   3.161 +(*...we assume X is a recent message and handle this case by contradiction*)
   3.162 +by (blast_tac (claset() addSEs knows_Spy_partsEs
   3.163 +                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   3.164 +val lemma = result();
   3.165 +
   3.166 +Goal "[| Says Server A                                                 \
   3.167 +\         {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs;  \
   3.168 +\       Says Server A'                                                 \
   3.169 +\         {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
   3.170 +\       evs : yahalom |]                                    \
   3.171 +\    ==> A=A' & B=B' & na=na' & nb=nb'";
   3.172 +by (prove_unique_tac lemma 1);
   3.173 +qed "unique_session_keys";
   3.174 +
   3.175 +
   3.176 +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   3.177 +
   3.178 +Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]                \
   3.179 +\     ==> Says Server A                                        \
   3.180 +\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   3.181 +\             Crypt (shrK B) {|Agent A, Key K|}|}              \
   3.182 +\          : set evs -->                                       \
   3.183 +\         Key K ~: analz (knows Spy evs)";
   3.184 +by (etac yahalom.induct 1);
   3.185 +by analz_knows_Spy_tac;
   3.186 +by (ALLGOALS
   3.187 +    (asm_simp_tac 
   3.188 +     (simpset() addsimps split_ifs @ pushes @
   3.189 +                         [analz_insert_eq, analz_insert_freshK])));
   3.190 +(*YM3*)
   3.191 +by (blast_tac (claset() delrules [impCE]
   3.192 +                        addSEs knows_Spy_partsEs
   3.193 +                        addIs [impOfSubs analz_subset_parts]) 2);
   3.194 +(*Fake*) 
   3.195 +by (spy_analz_tac 1);
   3.196 +val lemma = result() RS mp RSN(2,rev_notE);
   3.197 +
   3.198 +
   3.199 +(*Final version*)
   3.200 +Goal "[| Says Server A                                         \
   3.201 +\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   3.202 +\             Crypt (shrK B) {|Agent A, Key K|}|}              \
   3.203 +\          : set evs;                                          \
   3.204 +\        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   3.205 +\     ==> Key K ~: analz (knows Spy evs)";
   3.206 +by (blast_tac (claset() addSEs [lemma]) 1);
   3.207 +qed "Spy_not_see_encrypted_key";
   3.208 +
   3.209 +
   3.210 +(** Security Guarantee for A upon receiving YM3 **)
   3.211 +
   3.212 +(*If the encrypted message appears then it originated with the Server*)
   3.213 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   3.214 +\        A ~: bad;  evs : yahalom |]                          \
   3.215 +\      ==> Says Server A                                      \
   3.216 +\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|},      \
   3.217 +\             Crypt (shrK B) {|Agent A, Key K|}|}             \
   3.218 +\          : set evs";
   3.219 +by (etac rev_mp 1);
   3.220 +by (parts_induct_tac 1);
   3.221 +by (Fake_parts_insert_tac 1);
   3.222 +qed "A_trusts_YM3";
   3.223 +
   3.224 +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   3.225 +Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (knows Spy evs); \
   3.226 +\        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   3.227 +\     ==> Key K ~: analz (knows Spy evs)";
   3.228 +by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
   3.229 +qed "A_gets_good_key";
   3.230 +
   3.231 +(** Security Guarantees for B upon receiving YM4 **)
   3.232 +
   3.233 +(*B knows, by the first part of A's message, that the Server distributed 
   3.234 +  the key for A and B.  But this part says nothing about nonces.*)
   3.235 +Goal "[| Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs);  \
   3.236 +\        B ~: bad;  evs : yahalom |]                                 \
   3.237 +\     ==> EX NA NB. Says Server A                                    \
   3.238 +\                     {|Crypt (shrK A) {|Agent B, Key K,             \
   3.239 +\                                        Nonce NA, Nonce NB|},       \
   3.240 +\                       Crypt (shrK B) {|Agent A, Key K|}|}          \
   3.241 +\                    : set evs";
   3.242 +by (etac rev_mp 1);
   3.243 +by (parts_induct_tac 1);
   3.244 +by (Fake_parts_insert_tac 1);
   3.245 +(*YM3*)
   3.246 +by (Blast_tac 1);
   3.247 +qed "B_trusts_YM4_shrK";
   3.248 +
   3.249 +(** Up to now, the reasoning is similar to standard Yahalom.  Now the
   3.250 +    doubtful reasoning occurs.  We should not be assuming that an unknown
   3.251 +    key is secure, but the model allows us to: there is no Oops rule to
   3.252 +    let session keys go.*)
   3.253 +
   3.254 +(*B knows, by the second part of A's message, that the Server distributed 
   3.255 +  the key quoting nonce NB.  This part says nothing about agent names. 
   3.256 +  Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)
   3.257 +  the secrecy of NB.*)
   3.258 +Goal "evs : yahalom                                          \
   3.259 +\     ==> Key K ~: analz (knows Spy evs) -->                 \
   3.260 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->     \
   3.261 +\         (EX A B NA. Says Server A                          \
   3.262 +\                     {|Crypt (shrK A) {|Agent B, Key K,     \
   3.263 +\                               Nonce NA, Nonce NB|},        \
   3.264 +\                       Crypt (shrK B) {|Agent A, Key K|}|}  \
   3.265 +\                    : set evs)";
   3.266 +by (parts_induct_tac 1);
   3.267 +by (ALLGOALS Clarify_tac);
   3.268 +(*YM3 & Fake*)
   3.269 +by (Blast_tac 2);
   3.270 +by (Fake_parts_insert_tac 1);
   3.271 +(*YM4*)
   3.272 +(*A is uncompromised because NB is secure*)
   3.273 +by (g_not_bad_tac "A" 1);
   3.274 +(*A's certificate guarantees the existence of the Server message*)
   3.275 +by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj RS parts.Fst RS
   3.276 +			       A_trusts_YM3]) 1);
   3.277 +bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   3.278 +
   3.279 +
   3.280 +(*B's session key guarantee from YM4.  The two certificates contribute to a
   3.281 +  single conclusion about the Server's message. *)
   3.282 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                    \
   3.283 +\                 Crypt K (Nonce NB)|} : set evs;                       \
   3.284 +\        Says B Server                                                  \
   3.285 +\          {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
   3.286 +\          : set evs;                                                   \
   3.287 +\        A ~: bad;  B ~: bad;  evs : yahalom |]                         \
   3.288 +\      ==> EX na nb. Says Server A                                      \
   3.289 +\                  {|Crypt (shrK A) {|Agent B, Key K, na, nb|},         \
   3.290 +\                    Crypt (shrK B) {|Agent A, Key K|}|}                \
   3.291 +\            : set evs";
   3.292 +by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN
   3.293 +    assume_tac 1 THEN dtac B_trusts_YM4_shrK 1);
   3.294 +by (dtac B_trusts_YM4_newK 3);
   3.295 +by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   3.296 +by (etac Spy_not_see_encrypted_key 1 THEN REPEAT (assume_tac 1));
   3.297 +by (forward_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
   3.298 +by (blast_tac (claset() addDs []) 1);
   3.299 +qed "B_trusts_YM4";
   3.300 +
   3.301 +
   3.302 +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   3.303 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                   \
   3.304 +\                    Crypt K (Nonce NB)|} : set evs;                   \
   3.305 +\        Says B Server                                                 \
   3.306 +\          {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   3.307 +\          : set evs;                                                  \
   3.308 +\        A ~: bad;  B ~: bad;  evs : yahalom |]                \
   3.309 +\     ==> Key K ~: analz (knows Spy evs)";
   3.310 +by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
   3.311 +qed "B_gets_good_key";
   3.312 +
   3.313 +
   3.314 +(*** Authenticating B to A: these proofs are not considered.
   3.315 +     They are irrelevant to showing the need for Oops. ***)
   3.316 +
   3.317 +
   3.318 +(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   3.319 +
   3.320 +(*Assuming the session key is secure, if both certificates are present then
   3.321 +  A has said NB.  We can't be sure about the rest of A's message, but only
   3.322 +  NB matters for freshness.*)  
   3.323 +Goal "evs : yahalom                                              \
   3.324 +\     ==> Key K ~: analz (knows Spy evs) -->                     \
   3.325 +\         Crypt K (Nonce NB) : parts (knows Spy evs) -->         \
   3.326 +\         Crypt (shrK B) {|Agent A, Key K|} : parts (knows Spy evs) --> \
   3.327 +\         B ~: bad -->                                           \
   3.328 +\         (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   3.329 +by (parts_induct_tac 1);
   3.330 +(*Fake*)
   3.331 +by (Fake_parts_insert_tac 1);
   3.332 +(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   3.333 +by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
   3.334 +(*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   3.335 +by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   3.336 +(*yes: apply unicity of session keys*)
   3.337 +by (g_not_bad_tac "Aa" 1);
   3.338 +by (blast_tac (claset() addSEs [MPair_parts]
   3.339 +                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   3.340 +		        addDs  [Says_imp_knows_Spy RS parts.Inj,
   3.341 +				unique_session_keys]) 1);
   3.342 +qed_spec_mp "A_Said_YM3_lemma";
   3.343 +
   3.344 +(*If B receives YM4 then A has used nonce NB (and therefore is alive).
   3.345 +  Moreover, A associates K with NB (thus is talking about the same run).
   3.346 +  Other premises guarantee secrecy of K.*)
   3.347 +Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},                   \
   3.348 +\                 Crypt K (Nonce NB)|} : set evs;                      \
   3.349 +\        Says B Server                                                 \
   3.350 +\          {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   3.351 +\          : set evs;                                                  \
   3.352 +\        A ~: bad;  B ~: bad;  evs : yahalom |]       \
   3.353 +\     ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   3.354 +by (forward_tac [B_trusts_YM4] 1);
   3.355 +by (REPEAT_FIRST assume_tac);
   3.356 +by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1);
   3.357 +by (Clarify_tac 1);
   3.358 +by (rtac A_Said_YM3_lemma 1);
   3.359 +by (rtac Spy_not_see_encrypted_key 2);
   3.360 +by (REPEAT_FIRST assume_tac);
   3.361 +qed_spec_mp "YM4_imp_A_Said_YM3";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Thu Mar 18 10:41:33 1999 +0100
     4.3 @@ -0,0 +1,66 @@
     4.4 +(*  Title:      HOL/Auth/Yahalom
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1996  University of Cambridge
     4.8 +
     4.9 +Inductive relation "yahalom" for the Yahalom protocol.
    4.10 +
    4.11 +Example of why Oops is necessary.  This protocol can be attacked because it
    4.12 +doesn't keep NB secret, but without Oops it can be "verified" anyway.
    4.13 +*)
    4.14 +
    4.15 +Yahalom_Bad = Shared + 
    4.16 +
    4.17 +consts  yahalom   :: event list set
    4.18 +inductive "yahalom"
    4.19 +  intrs 
    4.20 +         (*Initial trace is empty*)
    4.21 +    Nil  "[]: yahalom"
    4.22 +
    4.23 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    4.24 +           invent new nonces here, but he can also use NS1.  Common to
    4.25 +           all similar protocols.*)
    4.26 +    Fake "[| evs: yahalom;  X: synth (analz (knows Spy evs)) |]
    4.27 +          ==> Says Spy B X  # evs : yahalom"
    4.28 +
    4.29 +         (*A message that has been sent can be received by the
    4.30 +           intended recipient.*)
    4.31 +    Reception "[| evsr: yahalom;  Says A B X : set evsr |]
    4.32 +               ==> Gets B X # evsr : yahalom"
    4.33 +
    4.34 +         (*Alice initiates a protocol run*)
    4.35 +    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
    4.36 +          ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    4.37 +
    4.38 +         (*Bob's response to Alice's message.*)
    4.39 +    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
    4.40 +             Gets B {|Agent A, Nonce NA|} : set evs2 |]
    4.41 +          ==> Says B Server 
    4.42 +                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    4.43 +                # evs2 : yahalom"
    4.44 +
    4.45 +         (*The Server receives Bob's message.  He responds by sending a
    4.46 +            new session key to Alice, with a packet for forwarding to Bob.*)
    4.47 +    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
    4.48 +             Gets Server 
    4.49 +                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    4.50 +               : set evs3 |]
    4.51 +          ==> Says Server A
    4.52 +                   {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    4.53 +                     Crypt (shrK B) {|Agent A, Key KAB|}|}
    4.54 +                # evs3 : yahalom"
    4.55 +
    4.56 +         (*Alice receives the Server's (?) message, checks her Nonce, and
    4.57 +           uses the new session key to send Bob his Nonce.  The premise
    4.58 +           A ~= Server is needed to prove Says_Server_not_range.*)
    4.59 +    YM4  "[| evs4: yahalom;  A ~= Server;
    4.60 +             Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
    4.61 +                : set evs4;
    4.62 +             Says A B {|Agent A, Nonce NA|} : set evs4 |]
    4.63 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    4.64 +
    4.65 +         (*This message models possible leaks of session keys.  The Nonces
    4.66 +           identify the protocol run.  Quoting Server here ensures they are
    4.67 +           correct.*)
    4.68 +
    4.69 +end