src/HOL/Auth/Event.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Event
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     2
    ID:         $Id$
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     5
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     6
Theory of events for security protocols
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     7
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     8
Datatype of events; function "sees"; freshness
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     9
*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    10
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    11
open Event;
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    12
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    13
(*** Function "sees" ***)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    14
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    15
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    16
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    17
goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    18
by (Simp_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    19
qed "sees_own";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    20
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    21
goal thy "sees lost B (Notes A X # evs) = \
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    22
\         (if A=B then insert X (sees lost B evs) else sees lost B evs)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    23
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    24
qed "sees_Notes";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    25
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    26
(** Three special-case rules for rewriting of sees lost A **)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    27
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    28
goal thy "!!A. Server ~= B ==> \
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    29
\          sees lost Server (Says A B X # evs) = sees lost Server evs";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    30
by (Asm_simp_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    31
qed "sees_Server";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    32
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    33
goal thy "!!A. Friend i ~= B ==> \
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    34
\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    35
by (Asm_simp_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    36
qed "sees_Friend";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    37
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    38
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    39
by (Simp_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    40
qed "sees_Spy";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    41
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    42
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    43
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    44
by (Fast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    45
qed "sees_Says_subset_insert";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    46
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    47
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    48
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    49
by (Fast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    50
qed "sees_subset_sees_Says";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    51
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    52
goal thy "sees lost A evs <= sees lost A (Notes A' X # evs)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    53
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    54
by (Fast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    55
qed "sees_subset_sees_Notes";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    56
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    57
(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    58
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    59
\         parts {Y} Un (UN A. parts (sees lost A evs))";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    60
by (Step_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    61
by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    62
by (ALLGOALS
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    63
    (fast_tac (!claset addss (!simpset addsimps [parts_Un] 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    64
				       setloop split_tac [expand_if]))));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    65
qed "UN_parts_sees_Says";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    66
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    67
goal thy "(UN A. parts (sees lost A (Notes B Y # evs))) = \
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    68
\         parts {Y} Un (UN A. parts (sees lost A evs))";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    69
by (Step_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    70
by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    71
by (ALLGOALS
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    72
    (fast_tac (!claset addss (!simpset addsimps [parts_Un] 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    73
				       setloop split_tac [expand_if]))));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    74
qed "UN_parts_sees_Notes";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    75
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    76
goal thy "Says A B X : set evs --> X : sees lost Spy evs";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    77
by (list.induct_tac "evs" 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    78
by (Auto_tac ());
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    79
qed_spec_mp "Says_imp_sees_Spy";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    80
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    81
(*Use with addSEs to derive contradictions from old Says events containing
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    82
  items known to be fresh*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    83
val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    84
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    85
Addsimps [sees_own, sees_Notes, sees_Server, sees_Friend, sees_Spy];
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    86
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    87
(**** NOTE REMOVAL--laws above are cleaner--def of sees1 is messy ****)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    88
Delsimps [sees_Cons];   
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    89
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    90
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    91
(*** Fresh nonces ***)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    92
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    93
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    94
by (etac (impOfSubs parts_mono) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    95
by (Fast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    96
qed "usedI";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    97
AddIs [usedI];
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    98
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    99
goal thy "used (Says A B X # evs) = parts{X} Un used evs";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   100
by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   101
qed "used_Says";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   102
Addsimps [used_Says];
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   103
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   104
goal thy "used (Notes A X # evs) = parts{X} Un used evs";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   105
by (simp_tac (!simpset delsimps [sees_Notes]
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   106
		       addsimps [used_def, UN_parts_sees_Notes]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   107
qed "used_Notes";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   108
Addsimps [used_Notes];
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   109
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   110
(*These two facts about "used" are unused.*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   111
goal thy "used [] <= used l";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   112
by (list.induct_tac "l" 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   113
by (event.induct_tac "a" 2);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   114
by (ALLGOALS Asm_simp_tac);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   115
by (ALLGOALS Blast_tac);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   116
qed "used_nil_subset";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   117
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   118
goal thy "used l <= used (l@l')";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   119
by (list.induct_tac "l" 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   120
by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   121
by (event.induct_tac "a" 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   122
by (ALLGOALS Asm_simp_tac);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   123
by (ALLGOALS Blast_tac);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   124
qed "used_subset_append";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   125
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   126
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   127
(** Simplifying   parts (insert X (sees lost A evs))
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   128
      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   129
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   130
val parts_insert_sees = 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   131
    parts_insert |> read_instantiate_sg (sign_of thy)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   132
                                        [("H", "sees lost A evs")]
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   133
                 |> standard;
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   134
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   135
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   136
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   137
(*For proving theorems of the form X ~: analz (sees Spy evs) --> P
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   138
  New events added by induction to "evs" are discarded.  Provided 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   139
  this information isn't needed, the proof will be much shorter, since
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   140
  it will omit complicated reasoning about analz.*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   141
val analz_mono_contra_tac = 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   142
  let val impI' = read_instantiate_sg (sign_of thy)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   143
                [("P", "?Y ~: analz (sees lost ?A ?evs)")] impI;
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   144
  in
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   145
    rtac impI THEN' 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   146
    REPEAT1 o 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   147
      (dresolve_tac 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   148
       [sees_subset_sees_Says  RS analz_mono RS contra_subsetD,
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   149
	sees_subset_sees_Notes RS analz_mono RS contra_subsetD])
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   150
    THEN'
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   151
    mp_tac
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
   152
  end;