Proof of Says_imp_old_keys is now more robust
authorpaulson
Mon Sep 23 18:20:43 1996 +0200 (1996-09-23)
changeset 20134b7a432fb3ed
parent 2012 1b234f1fd9c7
child 2014 5be4c8ca7b25
Proof of Says_imp_old_keys is now more robust
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Sep 23 18:19:38 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Sep 23 18:20:43 1996 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  HOL_quantifiers := false;
     1.5  
     1.6  
     1.7 -(** Weak liveness: there are traces that reach the end **)
     1.8 +(*Weak liveness: there are traces that reach the end*)
     1.9  
    1.10  goal thy 
    1.11   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.12 @@ -26,7 +26,7 @@
    1.13  br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
    1.14  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.15  by (ALLGOALS Fast_tac);
    1.16 -qed "weak_liveness";
    1.17 +result();
    1.18  
    1.19  
    1.20  (**** Inductive proofs about yahalom ****)
    1.21 @@ -49,13 +49,6 @@
    1.22  Addsimps [not_Says_to_self];
    1.23  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.24  
    1.25 -goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs";
    1.26 -be yahalom.induct 1;
    1.27 -by (Auto_tac());
    1.28 -qed "not_Notes";
    1.29 -Addsimps [not_Notes];
    1.30 -AddSEs   [not_Notes RSN (2, rev_notE)];
    1.31 -
    1.32  
    1.33  (** For reasoning about the encrypted portion of messages **)
    1.34  
    1.35 @@ -74,7 +67,8 @@
    1.36  
    1.37  
    1.38  
    1.39 -(*** Shared keys are not betrayed ***)
    1.40 +(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    1.41 +    sends messages containing X! **)
    1.42  
    1.43  (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    1.44  goal thy 
    1.45 @@ -148,8 +142,9 @@
    1.46  \           evs : yahalom                 \
    1.47  \        |] ==> length evt < length evs";
    1.48  br ccontr 1;
    1.49 +bd leI 1;
    1.50  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
    1.51 -	              addIs [impOfSubs parts_mono, leI]) 1);
    1.52 +                      addIs  [impOfSubs parts_mono]) 1);
    1.53  qed "Says_imp_old_keys";
    1.54  
    1.55  
    1.56 @@ -302,71 +297,83 @@
    1.57  qed "analz_insert_Key_newK";
    1.58  
    1.59  
    1.60 -(*Describes the form *and age* of K when the following message is sent*)
    1.61 +(*Describes the form of K when the Server sends this message.*)
    1.62  goal thy 
    1.63   "!!evs. [| Says Server A                                           \
    1.64  \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
    1.65  \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
    1.66  \           evs : yahalom |]                                        \
    1.67 -\        ==> (EX evt:yahalom. K = Key(newK evt) &                   \
    1.68 -\                           length evt < length evs)";
    1.69 +\        ==> (EX evt:yahalom. K = Key(newK evt))";
    1.70  be rev_mp 1;
    1.71  be yahalom.induct 1;
    1.72 -by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
    1.73 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.74  qed "Says_Server_message_form";
    1.75  
    1.76  
    1.77 -(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3
    1.78 -  As with Otway-Rees, proof does not need uniqueness of session keys.*)
    1.79 +(** Crucial secrecy property: Enemy does not see the keys sent in msg YM3
    1.80 +    As with Otway-Rees, proof does not need uniqueness of session keys. **)
    1.81 +
    1.82 +goal thy 
    1.83 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom;  evt : yahalom |]        \
    1.84 +\        ==> Says Server A                                                \
    1.85 +\              {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A),       \
    1.86 +\                Crypt {|Agent A, Key(newK evt)|} (shrK B)|}              \
    1.87 +\             : set_of_list evs -->    \
    1.88 +\            Key(newK evt) ~: analz (sees Enemy evs)";
    1.89 +be yahalom.induct 1;
    1.90 +bd YM4_analz_sees_Enemy 6;
    1.91 +by (ALLGOALS
    1.92 +    (asm_simp_tac 
    1.93 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.94 +			  analz_insert_Key_newK] @ pushes)
    1.95 +               setloop split_tac [expand_if])));
    1.96 +(*YM4*)
    1.97 +by (enemy_analz_tac 3);
    1.98 +(*YM3*)
    1.99 +by (fast_tac (!claset addIs [parts_insertI]
   1.100 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.101 +	              addss (!simpset)) 2);
   1.102 +(*Fake*) (** LEVEL 10 **)
   1.103 +by (enemy_analz_tac 1);
   1.104 +val lemma = result() RS mp RSN(2,rev_notE);
   1.105 +
   1.106 +
   1.107 +(*Final version: Server's message in the most abstract form*)
   1.108  goal thy 
   1.109   "!!evs. [| Says Server A \
   1.110  \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   1.111  \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   1.112  \           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
   1.113  \     K ~: analz (sees Enemy evs)";
   1.114 -be rev_mp 1;
   1.115 -be yahalom.induct 1;
   1.116 -bd YM4_analz_sees_Enemy 6;
   1.117 -by (ALLGOALS Asm_simp_tac);
   1.118 -(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.119 -by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.120 -by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   1.121 -by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   1.122 -by (ALLGOALS
   1.123 -    (asm_full_simp_tac 
   1.124 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.125 -			  analz_insert_Key_newK] @ pushes)
   1.126 -               setloop split_tac [expand_if])));
   1.127 -(*YM4*)
   1.128 -by (enemy_analz_tac 3);
   1.129 -(*YM3*)
   1.130 -by (fast_tac (!claset addSEs [less_irrefl]) 2);
   1.131 -(*Fake*) (** LEVEL 10 **)
   1.132 -by (enemy_analz_tac 1);
   1.133 +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.134 +by (fast_tac (!claset addSEs [lemma]) 1);
   1.135  qed "Enemy_not_see_encrypted_key";
   1.136  
   1.137  
   1.138 +(** Towards proofs of stronger authenticity properties **)
   1.139 +
   1.140  goal thy 
   1.141 - "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : analz (sees Enemy evs); \
   1.142 + "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees Enemy evs); \
   1.143  \           B ~: bad;  evs : yahalom |]                                 \
   1.144  \        ==> EX NA NB. Says Server A                                    \
   1.145 -\                     {|Crypt {|Agent B, Key K,                         \
   1.146 -\                               Nonce NA, Nonce NB|} (shrK A),          \
   1.147 -\                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   1.148 -\                   : set_of_list evs";
   1.149 +\                        {|Crypt {|Agent B, Key K,                      \
   1.150 +\                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.151 +\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   1.152 +\                       : set_of_list evs";
   1.153  be rev_mp 1;
   1.154  be yahalom.induct 1;
   1.155 -by (forward_tac [YM4_analz_sees_Enemy] 6);
   1.156 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   1.157 -(*YM4*)
   1.158 -by (enemy_analz_tac 4);
   1.159 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.160 +by (ALLGOALS Asm_simp_tac);
   1.161  (*YM3*)
   1.162  by (Fast_tac 3);
   1.163 -(*Fake*)
   1.164 -by (enemy_analz_tac 2);
   1.165  (*Base case*)
   1.166  by (fast_tac (!claset addss (!simpset)) 1);
   1.167 -qed "Enemy_analz_Server_msg";
   1.168 +(*Prepare YM4*)
   1.169 +by (stac insert_commute 2 THEN Simp_tac 2);
   1.170 +(*Fake and YM4 are similar*)
   1.171 +by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.172 +					impOfSubs Fake_parts_insert])));
   1.173 +qed "Crypt_imp_Server_msg";
   1.174  
   1.175  
   1.176  (*What can B deduce from receipt of YM4?  
   1.177 @@ -383,14 +390,10 @@
   1.178  \                   : set_of_list evs";
   1.179  be rev_mp 1;
   1.180  be yahalom.induct 1;
   1.181 -by (forward_tac [YM4_analz_sees_Enemy] 6);
   1.182 +by (dresolve_tac [YM4_analz_sees_Enemy] 6);
   1.183  by (ALLGOALS Asm_simp_tac);
   1.184 -(*YM4*)
   1.185 -by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 3);
   1.186 -(*YM3*)
   1.187 -by (Fast_tac 2);
   1.188 -(*Fake*)
   1.189 -by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 1);
   1.190 +by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS
   1.191 +					Crypt_imp_Server_msg])));
   1.192  qed "YM4_imp_Says_Server_A";
   1.193  
   1.194