src/HOL/Auth/Shared.ML
author paulson
Thu, 26 Sep 1996 12:50:48 +0200
changeset 2032 1bbf1bdcaf56
parent 2026 0df5a96bf77e
child 2045 ae1030e66745
permissions -rw-r--r--
Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Message
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
     9
*)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    10
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    11
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    13
(****************DELETE****************)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    14
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    15
local
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    16
    fun string_of (a,0) = a
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    17
      | string_of (a,i) = a ^ "_" ^ string_of_int i;
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    18
in
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    19
  fun freeze_thaw th =
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    20
    let val fth = freezeT th
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    21
        val {prop,sign,...} = rep_thm fth
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    22
        fun mk_inst (Var(v,T)) = 
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    23
            (cterm_of sign (Var(v,T)),
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    24
             cterm_of sign (Free(string_of v, T)))
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    25
        val insts = map mk_inst (term_vars prop)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    26
        fun thaw th' = 
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    27
            th' |> forall_intr_list (map #2 insts)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    28
                |> forall_elim_list (map #1 insts)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    29
    in  (instantiate ([],insts) fth, thaw)  end;
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    30
end;
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    31
fun defer_tac i state = 
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    32
    let val (state',thaw) = freeze_thaw state
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    33
        val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    34
        val hyp::hyps' = drop(i-1,hyps)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    35
    in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    36
        |> implies_intr_list (take(i-1,hyps) @ hyps')
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    37
        |> thaw
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    38
        |> Sequence.single
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    39
    end
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    40
    handle Bind => Sequence.null;
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    41
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    42
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    43
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    44
2000
adb88d42f1bd Abstraction of enemy_analz_tac over its argument
paulson
parents: 1993
diff changeset
    45
(*GOALS.ML??*)
adb88d42f1bd Abstraction of enemy_analz_tac over its argument
paulson
parents: 1993
diff changeset
    46
fun prlim n = (goals_limit:=n; pr());
adb88d42f1bd Abstraction of enemy_analz_tac over its argument
paulson
parents: 1993
diff changeset
    47
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    48
(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    49
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    50
by (fast_tac (!claset addEs [equalityE]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    51
val subset_range_iff = result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    52
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    53
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    54
open Shared;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    55
1964
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    56
(*Holds because Friend is injective: thus cannot prove for all f*)
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    57
goal thy "(Friend x : Friend``A) = (x:A)";
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    58
by (Auto_tac());
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    59
qed "Friend_image_eq";
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    60
Addsimps [Friend_image_eq];
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    61
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    62
Addsimps [Un_insert_left, Un_insert_right];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    63
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    64
(*By default only o_apply is built-in.  But in the presence of eta-expansion
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    65
  this means that some terms displayed as (f o g) will be rewritten, and others
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    66
  will not!*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    67
Addsimps [o_def];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    68
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    69
(*** Basic properties of shrK and newK ***)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    70
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    71
(* invKey (shrK A) = shrK A *)
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    72
bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    73
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    74
(* invKey (newK evs) = newK evs *)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    75
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    76
Addsimps [invKey_shrK, invKey_newK];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    77
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    78
1993
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
    79
(*Injectiveness and freshness of new keys and nonces*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    80
AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    81
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    82
(** Rewrites should not refer to  initState(Friend i) 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    83
    -- not in normal form! **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    84
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    85
Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    86
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    87
goal thy "Key (newK evs) ~: parts (initState lost B)";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    88
by (agent.induct_tac "B" 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    89
by (Auto_tac ());
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    90
qed "newK_notin_initState";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    91
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    92
goal thy "Nonce (newN evs) ~: parts (initState lost B)";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    93
by (agent.induct_tac "B" 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    94
by (Auto_tac ());
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    95
qed "newN_notin_initState";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    96
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    97
AddIffs [newK_notin_initState, newN_notin_initState];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    98
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    99
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   100
by (agent.induct_tac "C" 1);
1993
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   101
by (auto_tac (!claset addIs [range_eqI], !simpset));
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   102
qed "keysFor_parts_initState";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   103
Addsimps [keysFor_parts_initState];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   104
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   105
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   106
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   107
qed "keysFor_image_Key";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   108
Addsimps [keysFor_image_Key];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   109
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
   110
goal thy "shrK A ~: newK``E";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   111
by (agent.induct_tac "A" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   112
by (Auto_tac ());
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
   113
qed "shrK_notin_image_newK";
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
   114
Addsimps [shrK_notin_image_newK];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   115
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   116
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   117
(*** Function "sees" ***)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   118
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   119
goal thy
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   120
    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   121
by (list.induct_tac "evs" 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   122
by (agent.induct_tac "A" 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   123
by (event.induct_tac "a" 2);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   124
by (Auto_tac ());
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   125
qed "sees_mono";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   126
1964
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
   127
(*Agents see their own shared keys!*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   128
goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   129
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   130
by (agent.induct_tac "A" 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   131
by (Auto_tac ());
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   132
qed_spec_mp "sees_own_shrK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   133
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   134
(*Spy sees shared keys of lost agents!*)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   135
goal thy "!!i. A: lost ==> Key (shrK A) : sees lost Spy evs";
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   136
by (list.induct_tac "evs" 1);
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   137
by (Auto_tac());
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   138
qed "Spy_sees_bad";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   139
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   140
AddSIs [sees_own_shrK, Spy_sees_bad];
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   141
2026
0df5a96bf77e Last working version prior to introduction of "lost"
paulson
parents: 2012
diff changeset
   142
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   143
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
2026
0df5a96bf77e Last working version prior to introduction of "lost"
paulson
parents: 2012
diff changeset
   144
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   145
goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   146
by (Simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   147
qed "sees_own";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   148
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   149
goal thy "!!A. Server ~= A ==> \
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   150
\              sees lost Server (Says A B X # evs) = sees lost Server evs";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   151
by (Asm_simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   152
qed "sees_Server";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   153
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   154
goal thy "!!A. Friend i ~= A ==> \
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   155
\              sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   156
by (Asm_simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   157
qed "sees_Friend";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   158
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   159
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   160
by (Simp_tac 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   161
qed "sees_Spy";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   162
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   163
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   164
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   165
by (Fast_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   166
qed "sees_Says_subset_insert";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   167
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   168
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   169
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   170
by (Fast_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   171
qed "sees_subset_sees_Says";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   172
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   173
(*Pushing Unions into parts; one of the A's equals B, and thus sees lost Y*)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   174
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   175
\         parts {Y} Un (UN A. parts (sees lost A evs))";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   176
by (Step_tac 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   177
by (etac rev_mp 1);     (*for some reason, split_tac does not work on assumptions*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   178
val ss = (!simpset addsimps [parts_Un, sees_Cons] 
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   179
                   setloop split_tac [expand_if]);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   180
by (ALLGOALS (fast_tac (!claset addss ss)));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   181
qed "UN_parts_sees_Says";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   182
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   183
goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   184
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   185
by (Auto_tac ());
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   186
qed_spec_mp "Says_imp_sees_Spy";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   187
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   188
Addsimps [Says_imp_sees_Spy];
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   189
AddIs    [Says_imp_sees_Spy];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   190
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   191
goal thy "initState lost C <= Key `` range shrK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   192
by (agent.induct_tac "C" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   193
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   194
qed "initState_subset";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   195
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   196
goal thy "X : sees lost C evs --> \
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   197
\          (EX A B. Says A B X : set_of_list evs) | \
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
   198
\          (EX A. X = Key (shrK A))";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   199
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   200
by (ALLGOALS Asm_simp_tac);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   201
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   202
by (rtac conjI 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   203
by (Fast_tac 2);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   204
by (event.induct_tac "a" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   205
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   206
by (ALLGOALS Fast_tac);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   207
qed_spec_mp "seesD";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   208
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   209
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy];
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   210
Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   211
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   212
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   213
goal thy "!!K. newK evs = invKey K ==> newK evs = K";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   214
by (rtac (invKey_eq RS iffD1) 1);
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   215
by (Simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   216
val newK_invKey = result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   217
1993
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   218
AddSDs [newK_invKey];
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   219
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   220
(** Rewrites to push in Key and Crypt messages, so that other messages can
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   221
    be pulled out using the analz_insert rules **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   222
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   223
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   224
                      insert_commute;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   225
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   226
val pushKeys = map (insComm "Key ?K") 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   227
                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   228
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   229
val pushCrypts = map (insComm "Crypt ?X ?K") 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   230
                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   231
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   232
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   233
val pushes = pushKeys@pushCrypts;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   234
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
   235
val pushKey_newK = insComm "Key (newK ?evs)"  "Key (shrK ?C)";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   236
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   237
1993
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   238
(*No premature instantiation of variables.  For proving weak liveness.*)
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   239
fun safe_solver prems =
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   240
    match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   241
    ORELSE' etac FalseE;
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   242
2000
adb88d42f1bd Abstraction of enemy_analz_tac over its argument
paulson
parents: 1993
diff changeset
   243
(*Analysis of Fake cases and of messages that forward unknown parts
adb88d42f1bd Abstraction of enemy_analz_tac over its argument
paulson
parents: 1993
diff changeset
   244
  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   245
fun spy_analz_tac i =
1993
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   246
  SELECT_GOAL 
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   247
   (EVERY [  (*push in occurrences of X...*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   248
           (REPEAT o CHANGED)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   249
             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   250
             (*...allowing further simplifications*)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   251
           simp_tac (!simpset setloop split_tac [expand_if]) 1,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   252
           REPEAT (resolve_tac [impI,notI] 1),
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   253
           dtac (impOfSubs Fake_analz_insert) 1,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   254
           eresolve_tac [asm_rl, synth.Inj] 1,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   255
           Fast_tac 1,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   256
           Asm_full_simp_tac 1,
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   257
           IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   258
           ]) i;
1993
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   259
77e7ef8e5c3b Addition of enemy_analz_tac and safe_solver
paulson
parents: 1967
diff changeset
   260
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   261
(** Simplifying   parts (insert X (sees lost A evs))
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   262
                = parts {X} Un parts (sees lost A evs) -- since general case loops*)
2012
1b234f1fd9c7 Removal of the Notes constructor
paulson
parents: 2000
diff changeset
   263
1b234f1fd9c7 Removal of the Notes constructor
paulson
parents: 2000
diff changeset
   264
val parts_insert_sees = 
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
   265
    parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees lost A evs")]
2012
1b234f1fd9c7 Removal of the Notes constructor
paulson
parents: 2000
diff changeset
   266
                 |> standard;