src/HOL/Auth/Message.ML
changeset 1885 a18a6dc14f76
parent 1852 289ce6cb5c84
child 1893 fa58f4a06f21
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Jul 26 12:18:50 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Jul 26 12:19:46 1996 +0200
     1.3 @@ -268,6 +268,8 @@
     1.4  AddSEs [MPair_analyze];
     1.5  AddDs  [analyze.Decrypt];
     1.6  
     1.7 +Addsimps [analyze.Inj];
     1.8 +
     1.9  goal thy "H <= analyze(H)";
    1.10  by (Fast_tac 1);
    1.11  qed "analyze_increasing";
    1.12 @@ -289,6 +291,13 @@
    1.13  qed "parts_analyze";
    1.14  Addsimps [parts_analyze];
    1.15  
    1.16 +goal thy "analyze (parts H) = parts H";
    1.17 +by (Auto_tac());
    1.18 +be analyze.induct 1;
    1.19 +by (Auto_tac());
    1.20 +qed "analyze_parts";
    1.21 +Addsimps [analyze_parts];
    1.22 +
    1.23  (*Monotonicity; Lemma 1 of Lowe*)
    1.24  goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";
    1.25  by (rtac lfp_mono 1);
    1.26 @@ -342,6 +351,17 @@
    1.27  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.28  qed "analyze_insert_Key";
    1.29  
    1.30 +goal thy "analyze (insert {|X,Y|} H) = \
    1.31 +\         insert {|X,Y|} (analyze (insert X (insert Y H)))";
    1.32 +br equalityI 1;
    1.33 +br subsetI 1;
    1.34 +be analyze.induct 1;
    1.35 +by (Auto_tac());
    1.36 +be analyze.induct 1;
    1.37 +by (ALLGOALS (deepen_tac (!claset addIs [analyze.Fst, analyze.Snd, analyze.Decrypt]) 0));
    1.38 +qed "analyze_insert_MPair";
    1.39 +
    1.40 +(*Can pull out enCrypted message if the Key is not known*)
    1.41  goal thy "!!H. Key (invKey K) ~: analyze H ==>  \
    1.42  \              analyze (insert (Crypt X K) H) = \
    1.43  \              insert (Crypt X K) (analyze H)";
    1.44 @@ -375,70 +395,31 @@
    1.45  by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
    1.46  qed "analyze_insert_Decrypt";
    1.47  
    1.48 +(*Case analysis: either the message is secure, or it is not!
    1.49 +  Use with expand_if;  apparently split_tac does not cope with patterns
    1.50 +  such as "analyze (insert (Crypt X' K) H)" *)
    1.51 +goal thy "analyze (insert (Crypt X' K) H) = \
    1.52 +\         (if (Key (invKey K)  : analyze H) then    \
    1.53 +\               insert (Crypt X' K) (analyze (insert X' H)) \
    1.54 +\          else insert (Crypt X' K) (analyze H))";
    1.55 +by (excluded_middle_tac "Key (invKey K)  : analyze H " 1);
    1.56 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [analyze_insert_Crypt, 
    1.57 +					       analyze_insert_Decrypt])));
    1.58 +qed "analyze_Crypt_if";
    1.59 +
    1.60  Addsimps [analyze_insert_Agent, analyze_insert_Nonce, 
    1.61 -	  analyze_insert_Key, analyze_insert_Crypt,
    1.62 -	  analyze_insert_Decrypt];
    1.63 -
    1.64 +	  analyze_insert_Key, analyze_insert_MPair, 
    1.65 +	  analyze_Crypt_if];
    1.66  
    1.67  (*This rule supposes "for the sake of argument" that we have the key.*)
    1.68  goal thy  "analyze (insert (Crypt X K) H) <=  \
    1.69 -\         insert (Crypt X K) (analyze (insert X H))";
    1.70 +\          insert (Crypt X K) (analyze (insert X H))";
    1.71  br subsetI 1;
    1.72  be analyze.induct 1;
    1.73  by (Auto_tac());
    1.74  qed "analyze_insert_Crypt_subset";
    1.75  
    1.76  
    1.77 -(** Rewrite rules for pulling out atomic parts of messages **)
    1.78 -
    1.79 -goal thy "analyze (insert X H) <= analyze (insert {|X,Y|} H)";
    1.80 -br subsetI 1;
    1.81 -be analyze.induct 1;
    1.82 -by (ALLGOALS (best_tac (!claset addIs [analyze.Fst]))); 
    1.83 -qed "analyze_insert_subset_MPair1";
    1.84 -
    1.85 -goal thy "analyze (insert Y H) <= analyze (insert {|X,Y|} H)";
    1.86 -br subsetI 1;
    1.87 -be analyze.induct 1;
    1.88 -by (ALLGOALS (best_tac (!claset addIs [analyze.Snd]))); 
    1.89 -qed "analyze_insert_subset_MPair2";
    1.90 -
    1.91 -goal thy "analyze (insert {|Agent agt,Y|} H) = \
    1.92 -\         insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))";
    1.93 -by (rtac equalityI 1);
    1.94 -by (best_tac (!claset addIs [analyze.Fst,
    1.95 -			     impOfSubs analyze_insert_subset_MPair2]) 2); 
    1.96 -br subsetI 1;
    1.97 -be analyze.induct 1;
    1.98 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.99 -qed "analyze_insert_Agent_MPair";
   1.100 -
   1.101 -goal thy "analyze (insert {|Nonce N,Y|} H) = \
   1.102 -\         insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))";
   1.103 -by (rtac equalityI 1);
   1.104 -by (best_tac (!claset addIs [analyze.Fst,
   1.105 -			     impOfSubs analyze_insert_subset_MPair2]) 2); 
   1.106 -br subsetI 1;
   1.107 -be analyze.induct 1;
   1.108 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.109 -qed "analyze_insert_Nonce_MPair";
   1.110 -
   1.111 -(*Can only pull out Keys if they are not needed to decrypt the rest*)
   1.112 -goalw thy [keysFor_def]
   1.113 -    "!!K. K ~: keysFor (analyze (insert Y H)) ==>  \
   1.114 -\         analyze (insert {|Key K, Y|} H) = \
   1.115 -\         insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))";
   1.116 -by (rtac equalityI 1);
   1.117 -by (best_tac (!claset addIs [analyze.Fst,
   1.118 -			     impOfSubs analyze_insert_subset_MPair2]) 2); 
   1.119 -br subsetI 1;
   1.120 -be analyze.induct 1;
   1.121 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.122 -qed "analyze_insert_Key_MPair";
   1.123 -
   1.124 -Addsimps [analyze_insert_Agent_MPair, analyze_insert_Nonce_MPair,
   1.125 -	  analyze_insert_Key_MPair];
   1.126 -
   1.127  (** Idempotence and transitivity **)
   1.128  
   1.129  goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";
   1.130 @@ -467,6 +448,29 @@
   1.131     "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H"
   1.132  *)
   1.133  
   1.134 +
   1.135 +(** A congruence rule for "analyze" **)
   1.136 +
   1.137 +goal thy "!!H. [| analyze G <= analyze G'; analyze H <= analyze H' \
   1.138 +\              |] ==> analyze (G Un H) <= analyze (G' Un H')";
   1.139 +by (Step_tac 1);
   1.140 +be analyze.induct 1;
   1.141 +by (ALLGOALS (best_tac (!claset addIs [analyze_mono RS subsetD])));
   1.142 +qed "analyze_subset_cong";
   1.143 +
   1.144 +goal thy "!!H. [| analyze G = analyze G'; analyze H = analyze H' \
   1.145 +\              |] ==> analyze (G Un H) = analyze (G' Un H')";
   1.146 +by (REPEAT_FIRST (ares_tac [equalityI, analyze_subset_cong]
   1.147 +	  ORELSE' etac equalityE));
   1.148 +qed "analyze_cong";
   1.149 +
   1.150 +
   1.151 +goal thy "!!H. analyze H = analyze H'  ==>    \
   1.152 +\              analyze (insert X H) = analyze (insert X H')";
   1.153 +by (asm_simp_tac (!simpset addsimps [insert_def] 
   1.154 +		           setloop (rtac analyze_cong)) 1);
   1.155 +qed "analyze_insert_cong";
   1.156 +
   1.157  (*If there are no pairs or encryptions then analyze does nothing*)
   1.158  goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
   1.159  \         analyze H = H";
   1.160 @@ -510,6 +514,10 @@
   1.161  by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));
   1.162  qed "synthesize_Un";
   1.163  
   1.164 +goal thy "insert X (synthesize H) <= synthesize(insert X H)";
   1.165 +by (fast_tac (!claset addEs [impOfSubs synthesize_mono]) 1);
   1.166 +qed "synthesize_insert";
   1.167 +
   1.168  (** Idempotence and transitivity **)
   1.169  
   1.170  goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";
   1.171 @@ -539,6 +547,7 @@
   1.172    but can synthesize a pair or encryption from its components...*)
   1.173  val mk_cases = synthesize.mk_cases msg.simps;
   1.174  
   1.175 +(*NO Agent_synthesize, as any Agent name can be synthesized*)
   1.176  val Nonce_synthesize = mk_cases "Nonce n : synthesize H";
   1.177  val Key_synthesize   = mk_cases "Key K : synthesize H";
   1.178  val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H";
   1.179 @@ -566,14 +575,6 @@
   1.180  
   1.181  (*** Combinations of parts, analyze and synthesize ***)
   1.182  
   1.183 -(*Not that useful, in view of the following one...*)
   1.184 -goal thy "parts (synthesize H) <= synthesize (parts H)";
   1.185 -by (Step_tac 1);
   1.186 -be parts.induct 1;
   1.187 -be (parts_increasing RS synthesize_mono RS subsetD) 1;
   1.188 -by (ALLGOALS Fast_tac);
   1.189 -qed "parts_synthesize_subset";
   1.190 -
   1.191  goal thy "parts (synthesize H) = parts H Un synthesize H";
   1.192  br equalityI 1;
   1.193  br subsetI 1;