Spy can see Notes of the compromised agents
authorpaulson
Wed Sep 17 16:37:27 1997 +0200 (1997-09-17)
changeset 3678414e04d7c2d6
parent 3677 f2569416d18b
child 3679 8df171ccdbd8
Spy can see Notes of the compromised agents
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Wed Sep 17 16:37:21 1997 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Wed Sep 17 16:37:27 1997 +0200
     1.3 @@ -12,34 +12,59 @@
     1.4  
     1.5  AddIffs [Spy_in_lost, Server_not_lost];
     1.6  
     1.7 -(*** Function "sees" ***)
     1.8 +(**** Function "sees" ****)
     1.9  
    1.10 -(** Specialized rewrite rules for (sees A (Says...#evs)) **)
    1.11 +(** Specialized rewrite rules for (sees A' (Says A B X #evs)) **)
    1.12  
    1.13  goal thy "sees B (Says A B X # evs) = insert X (sees B evs)";
    1.14  by (Simp_tac 1);
    1.15 -qed "sees_own";
    1.16 -
    1.17 -goal thy "sees B (Notes A X # evs) = \
    1.18 -\         (if A=B then insert X (sees B evs) else sees B evs)";
    1.19 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.20 -qed "sees_Notes";
    1.21 +qed "sees_own_Says";
    1.22  
    1.23  (** Three special-case rules for rewriting of sees A **)
    1.24  
    1.25  goal thy "!!A. Server ~= B ==> \
    1.26 -\          sees Server (Says A B X # evs) = sees Server evs";
    1.27 +\              sees Server (Says A B X # evs) = sees Server evs";
    1.28  by (Asm_simp_tac 1);
    1.29 -qed "sees_Server";
    1.30 +qed "sees_Server_Says";
    1.31  
    1.32  goal thy "!!A. Friend i ~= B ==> \
    1.33 -\          sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
    1.34 +\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
    1.35  by (Asm_simp_tac 1);
    1.36 -qed "sees_Friend";
    1.37 +qed "sees_Friend_Says";
    1.38  
    1.39  goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
    1.40  by (Simp_tac 1);
    1.41 -qed "sees_Spy";
    1.42 +qed "sees_Spy_Says";
    1.43 +
    1.44 +
    1.45 +(** Specialized rewrite rules for (sees A' (Notes A X evs)) **)
    1.46 +
    1.47 +goal thy "sees A (Notes A X # evs) = insert X (sees A evs)";
    1.48 +by (Simp_tac 1);
    1.49 +qed "sees_own_Notes";
    1.50 +
    1.51 +(** Three special-case rules for rewriting of sees A **)
    1.52 +
    1.53 +goal thy "!!A. Server ~= A ==> \
    1.54 +\              sees Server (Notes A X # evs) = sees Server evs";
    1.55 +by (Asm_simp_tac 1);
    1.56 +qed "sees_Server_Notes";
    1.57 +
    1.58 +goal thy "!!A. Friend i ~= A ==> \
    1.59 +\              sees (Friend i) (Notes A X # evs) = sees (Friend i) evs";
    1.60 +by (Asm_simp_tac 1);
    1.61 +qed "sees_Friend_Notes";
    1.62 +
    1.63 +(*The point of letting the Spy see "lost" agents' notes is to prevent
    1.64 +  redundant case-splits on whether A=Spy and whether A:lost*)
    1.65 +goal thy "sees Spy (Notes A X # evs) = \
    1.66 +\         (if A:lost then insert X (sees Spy evs) else sees Spy evs)";
    1.67 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.68 +by (Blast_tac 1);
    1.69 +qed "sees_Spy_Notes";
    1.70 +
    1.71 +
    1.72 +(** Other "sees" lemmas **)
    1.73  
    1.74  goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
    1.75  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.76 @@ -75,16 +100,24 @@
    1.77  				       setloop split_tac [expand_if]))));
    1.78  qed "UN_parts_sees_Notes";
    1.79  
    1.80 +(*Spy sees all traffic*)
    1.81  goal thy "Says A B X : set evs --> X : sees Spy evs";
    1.82  by (induct_tac "evs" 1);
    1.83  by (Auto_tac ());
    1.84  qed_spec_mp "Says_imp_sees_Spy";
    1.85  
    1.86 +(*Spy sees Notes of lost agents*)
    1.87 +goal thy "Notes A X : set evs --> A: lost --> X : sees Spy evs";
    1.88 +by (induct_tac "evs" 1);
    1.89 +by (Auto_tac ());
    1.90 +qed_spec_mp "Notes_imp_sees_Spy";
    1.91 +
    1.92  (*Use with addSEs to derive contradictions from old Says events containing
    1.93    items known to be fresh*)
    1.94 -val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
    1.95 +val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj) :: partsEs;
    1.96  
    1.97 -Addsimps [sees_own, sees_Notes, sees_Server, sees_Friend, sees_Spy];
    1.98 +Addsimps [sees_own_Says, sees_Server_Says, sees_Friend_Says, sees_Spy_Says,
    1.99 +      sees_own_Notes, sees_Server_Notes, sees_Friend_Notes, sees_Spy_Notes];
   1.100  
   1.101  (**** NOTE REMOVAL--laws above are cleaner--def of sees1 is messy ****)
   1.102  Delsimps [sees_Cons];   
   1.103 @@ -104,8 +137,7 @@
   1.104  Addsimps [used_Says];
   1.105  
   1.106  goal thy "used (Notes A X # evs) = parts{X} Un used evs";
   1.107 -by (simp_tac (!simpset delsimps [sees_Notes]
   1.108 -		       addsimps [used_def, UN_parts_sees_Notes]) 1);
   1.109 +by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Notes]) 1);
   1.110  qed "used_Notes";
   1.111  Addsimps [used_Notes];
   1.112  
     2.1 --- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:21 1997 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:27 1997 +0200
     2.3 @@ -6,6 +6,9 @@
     2.4  Theory of events for security protocols
     2.5  
     2.6  Datatype of events; function "sees"; freshness
     2.7 +
     2.8 +"lost" agents have been broken by the Spy; their private keys and internal
     2.9 +    stores are visible to him
    2.10  *)
    2.11  
    2.12  Event = Message + List + 
    2.13 @@ -18,15 +21,7 @@
    2.14          | Notes agent       msg
    2.15  
    2.16  consts  
    2.17 -  sees1 :: [agent, event] => msg set
    2.18 -
    2.19 -primrec sees1 event
    2.20 -           (*Spy reads all traffic whether addressed to him or not*)
    2.21 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    2.22 -  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
    2.23 -
    2.24 -consts  
    2.25 -  lost :: agent set        (*agents whose private keys have been compromised*)
    2.26 +  lost :: agent set        (*compromised agents*)
    2.27    sees :: [agent, event list] => msg set
    2.28  
    2.29  rules
    2.30 @@ -34,6 +29,15 @@
    2.31    Spy_in_lost     "Spy: lost"
    2.32    Server_not_lost "Server ~: lost"
    2.33  
    2.34 +consts  
    2.35 +  sees1 :: [agent, event] => msg set
    2.36 +
    2.37 +primrec sees1 event
    2.38 +           (*Spy reads all traffic whether addressed to him or not*)
    2.39 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    2.40 +  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
    2.41 +					 else {})"
    2.42 +
    2.43  primrec sees list
    2.44    sees_Nil  "sees A []       = initState A"
    2.45    sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"