Incorporation of HPair into Message
authorpaulson
Tue Jan 07 16:28:43 1997 +0100 (1997-01-07)
changeset 2484596a5b5a68ff
parent 2483 95c2f9c0930a
child 2485 c4368c967c56
Incorporation of HPair into Message
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Jan 07 12:42:48 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Tue Jan 07 16:28:43 1997 +0100
     1.3 @@ -44,6 +44,49 @@
     1.4  Addsimps [invKey, invKey_eq];
     1.5  
     1.6  
     1.7 +(**** Freeness laws for HPair ****)
     1.8 +
     1.9 +goalw thy [HPair_def] "Agent A ~= HPair X Y";
    1.10 +by (Simp_tac 1);
    1.11 +qed "Agent_neq_HPair";
    1.12 +
    1.13 +goalw thy [HPair_def] "Nonce N ~= HPair X Y";
    1.14 +by (Simp_tac 1);
    1.15 +qed "Nonce_neq_HPair";
    1.16 +
    1.17 +goalw thy [HPair_def] "Key K ~= HPair X Y";
    1.18 +by (Simp_tac 1);
    1.19 +qed "Key_neq_HPair";
    1.20 +
    1.21 +goalw thy [HPair_def] "Hash Z ~= HPair X Y";
    1.22 +by (Simp_tac 1);
    1.23 +qed "Hash_neq_HPair";
    1.24 +
    1.25 +goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
    1.26 +by (Simp_tac 1);
    1.27 +qed "Crypt_neq_HPair";
    1.28 +
    1.29 +val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
    1.30 +		  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
    1.31 +
    1.32 +AddIffs HPair_neqs;
    1.33 +AddIffs (HPair_neqs RL [not_sym]);
    1.34 +
    1.35 +goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
    1.36 +by (Simp_tac 1);
    1.37 +qed "HPair_eq";
    1.38 +
    1.39 +goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
    1.40 +by (Simp_tac 1);
    1.41 +qed "MPair_eq_HPair";
    1.42 +
    1.43 +goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
    1.44 +by (Auto_tac());
    1.45 +qed "HPair_eq_MPair";
    1.46 +
    1.47 +AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
    1.48 +
    1.49 +
    1.50  (**** keysFor operator ****)
    1.51  
    1.52  goalw thy [keysFor_def] "keysFor {} = {}";
    1.53 @@ -752,6 +795,80 @@
    1.54  Addsimps [Hash_synth_analz];
    1.55  
    1.56  
    1.57 +(**** HPair: a combination of Hash and MPair ****)
    1.58 +
    1.59 +(*** Freeness ***)
    1.60 +
    1.61 +goalw thy [HPair_def] "Agent A ~= HPair X Y";
    1.62 +by (Simp_tac 1);
    1.63 +qed "Agent_neq_HPair";
    1.64 +
    1.65 +goalw thy [HPair_def] "Nonce N ~= HPair X Y";
    1.66 +by (Simp_tac 1);
    1.67 +qed "Nonce_neq_HPair";
    1.68 +
    1.69 +goalw thy [HPair_def] "Key K ~= HPair X Y";
    1.70 +by (Simp_tac 1);
    1.71 +qed "Key_neq_HPair";
    1.72 +
    1.73 +goalw thy [HPair_def] "Hash Z ~= HPair X Y";
    1.74 +by (Simp_tac 1);
    1.75 +qed "Hash_neq_HPair";
    1.76 +
    1.77 +goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
    1.78 +by (Simp_tac 1);
    1.79 +qed "Crypt_neq_HPair";
    1.80 +
    1.81 +val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
    1.82 +		  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
    1.83 +
    1.84 +AddIffs HPair_neqs;
    1.85 +AddIffs (HPair_neqs RL [not_sym]);
    1.86 +
    1.87 +goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
    1.88 +by (Simp_tac 1);
    1.89 +qed "HPair_eq";
    1.90 +
    1.91 +goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
    1.92 +by (Simp_tac 1);
    1.93 +qed "MPair_eq_HPair";
    1.94 +
    1.95 +goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
    1.96 +by (Auto_tac());
    1.97 +qed "HPair_eq_MPair";
    1.98 +
    1.99 +AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
   1.100 +
   1.101 +
   1.102 +(*** Specialized laws, proved in terms of those for Hash and MPair ***)
   1.103 +
   1.104 +goalw thy [HPair_def] "keysFor (insert (HPair X Y) H) = keysFor H";
   1.105 +by (Simp_tac 1);
   1.106 +qed "keysFor_insert_HPair";
   1.107 +
   1.108 +goalw thy [HPair_def]
   1.109 +    "parts (insert (HPair X Y) H) = \
   1.110 +\    insert (HPair X Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   1.111 +by (Simp_tac 1);
   1.112 +qed "parts_insert_HPair";
   1.113 +
   1.114 +goalw thy [HPair_def]
   1.115 +    "analz (insert (HPair X Y) H) = \
   1.116 +\    insert (HPair X Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   1.117 +by (Simp_tac 1);
   1.118 +qed "analz_insert_HPair";
   1.119 +
   1.120 +goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
   1.121 +\   ==> (HPair X Y : synth (analz H)) = \
   1.122 +\       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
   1.123 +by (Simp_tac 1);
   1.124 +by (Fast_tac 1);
   1.125 +qed "HPair_synth_analz";
   1.126 +
   1.127 +Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
   1.128 +	  HPair_synth_analz, HPair_synth_analz];
   1.129 +
   1.130 +
   1.131  (*We do NOT want Crypt... messages broken up in protocols!!*)
   1.132  Delrules partsEs;
   1.133  
   1.134 @@ -773,7 +890,8 @@
   1.135  val pushes = pushKeys@pushCrypts;
   1.136  
   1.137  
   1.138 -(*No premature instantiation of variables.  For proving weak liveness.*)
   1.139 +(*No premature instantiation of variables during simplification.
   1.140 +  For proving "possibility" properties.*)
   1.141  fun safe_solver prems =
   1.142      match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
   1.143      ORELSE' etac FalseE;
     2.1 --- a/src/HOL/Auth/Message.thy	Tue Jan 07 12:42:48 1997 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Tue Jan 07 16:28:43 1997 +0100
     2.3 @@ -48,7 +48,12 @@
     2.4    "{|x, y|}"      == "MPair x y"
     2.5  
     2.6  
     2.7 -constdefs  (*Keys useful to decrypt elements of a message set*)
     2.8 +constdefs
     2.9 +  (*Message Y, paired with a MAC computed with the help of X*)
    2.10 +  HPair :: "[msg,msg]=>msg"
    2.11 +    "HPair X Y == {| Hash{|X,Y|}, Y|}"
    2.12 +
    2.13 +  (*Keys useful to decrypt elements of a message set*)
    2.14    keysFor :: msg set => key set
    2.15    "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    2.16