Temporary additions (random) for the nested Otway-Rees protocol
authorpaulson
Fri Dec 13 10:42:58 1996 +0100 (1996-12-13)
changeset 2376f5c61fd9b9b6
parent 2375 14539397fc04
child 2377 ad9d2dedaeaa
Temporary additions (random) for the nested Otway-Rees protocol
They will need to be rationalized
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
     1.1 --- a/src/HOL/Auth/Shared.ML	Fri Dec 13 10:20:55 1996 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Fri Dec 13 10:42:58 1996 +0100
     1.3 @@ -26,19 +26,52 @@
     1.4  
     1.5  (*** Basic properties of shrK and newK ***)
     1.6  
     1.7 +goalw thy [newN_def] "!!evs. newN evs = newN evt ==> length evs = length evt";
     1.8 +by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
     1.9 +qed "newN_length";
    1.10 +
    1.11 +goalw thy [newK_def] "!!evs. newK evs = newK evt ==> length evs = length evt";
    1.12 +by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
    1.13 +qed "newK_length";
    1.14 +
    1.15 +goalw thy [newK_def] "newK evs ~= shrK A";
    1.16 +by (rtac random_neq_shrK 1);
    1.17 +qed "newK_neq_shrK";
    1.18 +
    1.19 +goalw thy [newK_def] "isSymKey (newK evs)";
    1.20 +by (rtac isSym_random 1);
    1.21 +qed "isSym_newK";
    1.22 +
    1.23  (* invKey (shrK A) = shrK A *)
    1.24  bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
    1.25  
    1.26 +(* invKey (random x) = random x *)
    1.27 +bind_thm ("invKey_random", rewrite_rule [isSymKey_def] isSym_random);
    1.28 +
    1.29  (* invKey (newK evs) = newK evs *)
    1.30  bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    1.31 -Addsimps [invKey_shrK, invKey_newK];
    1.32 +Addsimps [invKey_shrK, invKey_random, invKey_newK];
    1.33 +
    1.34 +goal thy "!!K. random x = invKey K ==> random x = K";
    1.35 +by (rtac (invKey_eq RS iffD1) 1);
    1.36 +by (Simp_tac 1);
    1.37 +val random_invKey = result();
    1.38  
    1.39 +AddSDs [random_invKey, sym RS random_invKey];
    1.40 +
    1.41 +goal thy "!!K. newK evs = invKey K ==> newK evs = K";
    1.42 +by (rtac (invKey_eq RS iffD1) 1);
    1.43 +by (Simp_tac 1);
    1.44 +val newK_invKey = result();
    1.45 +
    1.46 +AddSDs [newK_invKey, sym RS newK_invKey];
    1.47  
    1.48  (*Injectiveness and freshness of new keys and nonces*)
    1.49 -AddIffs [inj_shrK RS inj_eq];
    1.50 +AddIffs [inj_shrK RS inj_eq, inj_random RS inj_eq];
    1.51  AddSDs  [newN_length, newK_length];
    1.52  
    1.53 -Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
    1.54 +Addsimps [random_neq_shrK, random_neq_shrK RS not_sym,
    1.55 +	  newK_neq_shrK, newK_neq_shrK RS not_sym];
    1.56  
    1.57  (** Rewrites should not refer to  initState(Friend i) 
    1.58      -- not in normal form! **)
    1.59 @@ -72,6 +105,12 @@
    1.60  qed "shrK_notin_image_newK";
    1.61  Addsimps [shrK_notin_image_newK];
    1.62  
    1.63 +goal thy "shrK A ~: random``E";
    1.64 +by (agent.induct_tac "A" 1);
    1.65 +by (Auto_tac ());
    1.66 +qed "shrK_notin_image_random";
    1.67 +Addsimps [shrK_notin_image_random];
    1.68 +
    1.69  
    1.70  (*** Function "sees" ***)
    1.71  
    1.72 @@ -221,14 +260,6 @@
    1.73  (*Push newK applications in, allowing other keys to be pulled out*)
    1.74  val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
    1.75  
    1.76 -goal thy "!!K. newK evs = invKey K ==> newK evs = K";
    1.77 -by (rtac (invKey_eq RS iffD1) 1);
    1.78 -by (Simp_tac 1);
    1.79 -val newK_invKey = result();
    1.80 -
    1.81 -AddSDs [newK_invKey];
    1.82 -AddSDs [sym RS newK_invKey];
    1.83 -
    1.84  Delsimps [image_insert];
    1.85  Addsimps [image_insert RS sym];
    1.86  
     2.1 --- a/src/HOL/Auth/Shared.thy	Fri Dec 13 10:20:55 1996 +0100
     2.2 +++ b/src/HOL/Auth/Shared.thy	Fri Dec 13 10:42:58 1996 +0100
     2.3 @@ -44,19 +44,24 @@
     2.4    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
     2.5  
     2.6  
     2.7 -(*Agents generate "random" nonces and keys.  These are uniquely determined by
     2.8 -  the length of their argument, a trace.*)
     2.9 +(*Agents generate "random" numbers for use as symmetric keys, as well as
    2.10 +  nonces.*)
    2.11 +
    2.12  consts
    2.13 -  newN :: "event list => nat"
    2.14 -  newK :: "event list => key"
    2.15 +  random :: "nat*nat => nat"
    2.16 +
    2.17 +constdefs
    2.18 +  newN   :: event list => nat
    2.19 +  "newN evs == random (length evs, 0)"
    2.20 +
    2.21 +  newK   :: event list => nat
    2.22 +  "newK evs == random (length evs, 1)"
    2.23  
    2.24  rules
    2.25 -  inj_shrK      "inj shrK"
    2.26 +  inj_shrK        "inj shrK"
    2.27 +  inj_random      "inj random"
    2.28  
    2.29 -  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
    2.30 -  newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
    2.31 -
    2.32 -  newK_neq_shrK "newK evs ~= shrK A" 
    2.33 -  isSym_newK    "isSymKey (newK evs)"
    2.34 +  random_neq_shrK "random ij ~= shrK A" 
    2.35 +  isSym_random    "isSymKey (random ij)"
    2.36  
    2.37  end