src/HOL/Auth/Event.ML
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1852 289ce6cb5c84
child 1885 a18a6dc14f76
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Message
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     2
    ID:         $Id$
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     5
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     6
Datatype of events;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     7
inductive relation "traces" for Needham-Schroeder (shared keys)
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
     8
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
     9
Rewrites should not refer to	 initState (Friend i)    -- not in normal form
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    10
*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    11
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    12
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    13
open Event;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    14
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    15
(*Rewrite using   {a} Un A = insert a A *)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    16
Addsimps [insert_is_Un RS sym];
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    17
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    18
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    19
(*** Basic properties of serverKey and newK ***)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    20
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    21
(* invKey (serverKey A) = serverKey A *)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    22
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    23
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    24
(* invKey (newK evs) = newK evs *)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    25
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    26
Addsimps [invKey_serverKey, invKey_newK];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    27
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    28
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    29
(*New keys and nonces are fresh*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    30
val serverKey_inject = inj_serverKey RS injD;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    31
val newN_inject = inj_newN RS injD
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    32
and newK_inject = inj_newK RS injD;
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    33
AddSEs [serverKey_inject, newN_inject, newK_inject,
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    34
	fresh_newK RS notE, fresh_newN RS notE];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    35
Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    36
Addsimps [fresh_newN, fresh_newK];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    37
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    38
goal thy "newK evs ~= serverKey B";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    39
by (subgoal_tac "newK evs = serverKey B --> \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    40
\                Key (newK evs) : parts (initState B)" 1);
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    41
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    42
by (agent.induct_tac "B" 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    43
by (auto_tac (!claset addIs [range_eqI], !simpset));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    44
qed "newK_neq_serverKey";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    45
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    46
Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    47
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    48
(*Good for talking about Server's initial state*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    49
goal thy "parts (range (Key o f)) = range (Key o f)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    50
by (auto_tac (!claset addIs [range_eqI], !simpset));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    51
be parts.induct 1;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    52
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    53
qed "parts_range_Key";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    54
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    55
goal thy "analyze (range (Key o f)) = range (Key o f)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    56
by (auto_tac (!claset addIs [range_eqI], !simpset));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    57
be analyze.induct 1;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    58
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    59
qed "analyze_range_Key";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    60
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    61
Addsimps [parts_range_Key, analyze_range_Key];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    62
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    63
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    64
by (agent.induct_tac "C" 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    65
by (auto_tac (!claset addIs [range_eqI], !simpset));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    66
qed "keysFor_parts_initState";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    67
Addsimps [keysFor_parts_initState];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    68
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    69
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    70
(**** Inductive relation "traces" -- basic properties ****)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    71
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    72
val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    73
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    74
val Says_tracesE        = mk_cases "Says A B X # evs: traces";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    75
val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    76
val Says_Enemy_tracesE  = mk_cases "Says Enemy B X # evs: traces";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    77
val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    78
val Notes_tracesE       = mk_cases "Notes A X # evs: traces";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    79
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    80
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    81
(*The tail of a trace is a trace*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    82
goal thy "!!ev evs. ev#evs : traces ==> evs : traces";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    83
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    84
qed "traces_ConsE";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    85
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    86
(** Specialized rewrite rules for (sees A (Says...#evs)) **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    87
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    88
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    89
by (Simp_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    90
qed "sees_own";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    91
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    92
goal thy "!!A. Server ~= A ==> \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    93
\              sees Server (Says A B X # evs) = sees Server evs";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    94
by (Asm_simp_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    95
qed "sees_Server";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    96
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    97
goal thy "!!A. Friend i ~= A ==> \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    98
\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    99
by (Asm_simp_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   100
qed "sees_Friend";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   101
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   102
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   103
by (Simp_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   104
qed "sees_Enemy";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   105
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   106
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   107
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   108
by (Fast_tac 1);
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   109
qed "sees_Says_subset_insert";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   110
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   111
goal thy "sees A evs <= sees A (Says A' B X # evs)";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   112
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   113
by (Fast_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   114
qed "sees_subset_sees_Says";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   115
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   116
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   117
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   118
\         parts {Y} Un (UN A. parts (sees A evs))";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   119
by (Step_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   120
be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   121
val ss = (!simpset addsimps [parts_Un, sees_Cons] 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   122
	           setloop split_tac [expand_if]);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   123
by (ALLGOALS (fast_tac (!claset addss ss)));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   124
qed "UN_parts_sees_Says";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   125
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   126
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   127
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   128
Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   129
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   130
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   131
(**** Inductive proofs about traces ****)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   132
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   133
(*The Enemy can see more than anybody else, except for their initial state*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   134
goal thy 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   135
 "!!evs. evs : traces ==> \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   136
\     sees A evs <= initState A Un sees Enemy evs";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   137
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   138
be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   139
be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   140
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   141
			        addss (!simpset))));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   142
qed "sees_agent_subset_sees_Enemy";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   143
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   144
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   145
goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   146
be traces.induct 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   147
by (Auto_tac());
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   148
qed_spec_mp "not_Says_to_self";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   149
Addsimps [not_Says_to_self];
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   150
AddSEs   [not_Says_to_self RSN (2, rev_notE)];
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   151
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   152
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   153
(*** Server keys are not betrayed ***)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   154
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   155
(*Enemy never sees another agent's server key!*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   156
goal thy 
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   157
 "!!evs. [| evs : traces; A ~= Enemy |] ==> \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   158
\        Key (serverKey A) ~: parts (sees Enemy evs)";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   159
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   160
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   161
by (auto_tac(!claset, !simpset addsimps [parts_insert2]));
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   162
(*Deals with Faked messages*)
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   163
by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   164
			     impOfSubs parts_insert_subset_Un]
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   165
	              addss (!simpset)) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   166
qed "Enemy_not_see_serverKey";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   167
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   168
bind_thm ("Enemy_not_analyze_serverKey",
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   169
	  [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   170
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   171
Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey];
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   172
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   173
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   174
(*No Friend will ever see another agent's server key 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   175
  (excluding the Enemy, who might transmit his).*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   176
goal thy 
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   177
 "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   178
\        Key (serverKey A) ~: parts (sees (Friend j) evs)";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   179
br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   180
by (ALLGOALS Asm_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   181
qed "Friend_not_see_serverKey";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   182
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   183
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   184
(*** Future keys can't be seen or used! ***)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   185
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   186
(*Nobody can have SEEN keys that will be generated in the future.
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   187
  This has to be proved anew for each protocol description,
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   188
  but should go by similar reasoning every time.  Hardest case is the
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   189
  standard Fake rule.  
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   190
      The length comparison, and Union over C, are essential for the 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   191
  induction! *)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   192
goal thy "!!evs. evs : traces ==> \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   193
\                length evs <= length evs' --> \
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   194
\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   195
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   196
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   197
by (ALLGOALS (asm_full_simp_tac
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   198
	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   199
(*Initial state?  New keys cannot clash*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   200
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   201
(*Rule NS1 in protocol*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   202
by (fast_tac (!claset addDs [less_imp_le]) 2);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   203
(*Rule NS2 in protocol*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   204
by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   205
(*Rule NS3 in protocol*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   206
by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   207
(*Rule Fake: where an Enemy agent can say practically anything*)
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   208
by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   209
			     impOfSubs parts_insert_subset_Un,
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   210
			     less_imp_le]
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   211
	              addss (!simpset)) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   212
val lemma = result();
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   213
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   214
(*Variant needed for the main theorem below*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   215
goal thy 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   216
 "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   217
\        Key (newK evs') ~: parts (sees C evs)";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   218
by (fast_tac (!claset addDs [lemma]) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   219
qed "new_keys_not_seen";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   220
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   221
goal thy "!!K. newK evs = invKey K ==> newK evs = K";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   222
br (invKey_eq RS iffD1) 1;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   223
by (Simp_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   224
val newK_invKey = result();
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   225
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   226
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   227
val keysFor_parts_mono = parts_mono RS keysFor_mono;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   228
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   229
(*Nobody can have USED keys that will be generated in the future.
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   230
  ...very like new_keys_not_seen*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   231
goal thy "!!evs. evs : traces ==> \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   232
\                length evs <= length evs' --> \
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   233
\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   234
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   235
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   236
by (ALLGOALS (asm_full_simp_tac
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   237
	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   238
(*Rule NS1 in protocol*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   239
by (fast_tac (!claset addDs [less_imp_le]) 2);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   240
(*Rule NS2 in protocol*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   241
by (fast_tac (!claset addDs [less_imp_le]) 2);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   242
(*Rule Fake: where an Enemy agent can say practically anything*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   243
by (best_tac 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   244
    (!claset addSDs [newK_invKey]
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   245
	     addDs [impOfSubs (analyze_subset_parts RS keysFor_mono),
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   246
		    impOfSubs (parts_insert_subset_Un RS keysFor_mono),
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   247
		    less_imp_le]
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   248
             addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   249
	     addss (!simpset)) 1);
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   250
(*Rule NS3: quite messy...*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   251
by (hyp_subst_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   252
by (full_simp_tac (!simpset addcongs [conj_cong]) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   253
br impI 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   254
bd mp 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   255
by (fast_tac (!claset addDs [less_imp_le]) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   256
by (best_tac (!claset addIs 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   257
	      [impOfSubs (sees_subset_sees_Says RS keysFor_parts_mono),
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   258
	       impOfSubs (sees_own RS equalityD2 RS keysFor_parts_mono),
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   259
	       impOfSubs (empty_subsetI RS insert_mono RS keysFor_parts_mono)]
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   260
              addss (!simpset)) 1);
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   261
val lemma = result();
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   262
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   263
goal thy 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   264
 "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   265
\        newK evs' ~: keysFor (parts (sees C evs))";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   266
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   267
qed "new_keys_not_used";
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   268
Addsimps [new_keys_not_used];
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   269
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   270
bind_thm ("new_keys_not_analyzed",
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   271
	  [analyze_subset_parts RS keysFor_mono,
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   272
	   new_keys_not_used] MRS contra_subsetD);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   273
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   274
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   275
(*Maybe too specific to be of much use...*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   276
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   277
 "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   278
\                                (serverKey A))                  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   279
\               : setOfList evs;                                 \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   280
\           evs : traces    \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   281
\        |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   282
be rev_mp 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   283
be traces.induct 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   284
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   285
be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   286
by (ALLGOALS Asm_full_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   287
by (Fast_tac 1);	(*Proves the NS2 case*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   288
qed "Says_Server_imp_X_eq_Crypt";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   289
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   290
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   291
(*Pushes Crypt events in so that others might be pulled out*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   292
goal thy "insert (Crypt X K) (insert y evs) = \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   293
\         insert y (insert (Crypt X K) evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   294
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   295
qed "insert_Crypt_delay";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   296
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   297
goal thy "insert (Key K) (insert y evs) = \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   298
\         insert y (insert (Key K) evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   299
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   300
qed "insert_Key_delay";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   301
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   302
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   303
(** Lemmas concerning the form of items passed in messages **)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   304
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   305
(*Describes the form *and age* of K when the following message is sent*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   306
goal thy 
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   307
 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   308
\               : setOfList evs;  \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   309
\           evs : traces          \
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   310
\        |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   311
be rev_mp 1;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   312
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   313
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   314
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   315
qed "Says_Server_imp_Key_newK";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   316
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   317
(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   318
bind_thm ("not_parts_not_keysFor_analyze", 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   319
	  analyze_subset_parts RS keysFor_mono RS contra_subsetD);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   320
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   321
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   322
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   323
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   324
ZZZZZZZZZZZZZZZZ;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   325
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   326
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   327
(*Fake case below may need something like this...*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   328
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   329
 "!!evs. evs : traces ==>                             \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   330
\        ALL B X. Crypt X (serverKey B) : analyze (sees Enemy evs)  -->   \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   331
\        (EX A A'. Says A A' (Crypt X (serverKey B)) : setOfList evs";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   332
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   333
goal thy 
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   334
 "!!evs. evs : traces ==>                             \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   335
\        ALL NA B K X. Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B) :
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   336
                       analyze (sees Enemy evs)  -->   \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   337
\        (EX A A'. Says A A' (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B)) : setOfList evs";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   338
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   339
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   340
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   341
(*Describes the form of X when the following message is sent*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   342
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   343
 "!!evs. evs : traces ==>                             \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   344
\        ALL S A NA B K X.                            \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   345
\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   346
\            : setOfList evs  -->   \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   347
\        (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   348
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   349
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   350
by (Step_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   351
by (ALLGOALS Asm_full_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   352
(*Remaining cases are Fake, NS2 and NS3*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   353
by (Fast_tac 2);	(*Solves the NS2 case*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   354
(*The NS3 case needs the induction hypothesis twice!
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   355
    One application is to the X component of the most recent message.*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   356
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   357
be conjE 2;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   358
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent (Friend i)|} (serverKey B)" 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   359
by (eres_inst_tac [("V","?P|?Q")] thin_rl 3);	(*speeds the following step*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   360
by (Fast_tac 3);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   361
(*DELETE the first quantified formula: it's now useless*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   362
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   363
by (fast_tac (!claset addss (!simpset)) 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   364
(*Now for the Fake case*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   365
be disjE 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   366
(*The subcase of Fake, where the message in question is NOT the most recent*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   367
by (Best_tac 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   368
(*The subcase of Fake proved because server keys are kept secret*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   369
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   370
be Crypt_synthesize 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   371
be Key_synthesize 2;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   372
by (Asm_full_simp_tac 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   373
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   374
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   375
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   376
 1. !!evs B X evsa S A NA Ba K Xa.
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   377
       [| evsa : traces;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   378
          ! S A NA B K X.
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   379
             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) :
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   380
             setOfList evsa -->
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   381
             (? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   382
          B ~= Enemy;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   383
          Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey B) :
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   384
          analyze (sees Enemy evsa) |] ==>
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   385
       ? evs'. Xa = Crypt {|Key (newK evs'), Agent B|} (serverKey Ba)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   386
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   387
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   388
(*Split up the possibilities of that message being synthesized...*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   389
by (Step_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   390
by (Best_tac 6);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   391
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   392
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   393
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   394
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   395
by (Safe_step_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   396
by (Safe_step_tac 2);
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   397
by (ALLGOALS Asm_full_simp_tac);
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   398
by (REPEAT_FIRST (etac disjE));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   399
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   400
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   401
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   402
by (hyp_subst_tac 5);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   403
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   404
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   405
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   406
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   407
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   408
by (REPEAT (dtac spec 3));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   409
fe conjE;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   410
fe mp ;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   411
by (REPEAT (resolve_tac [refl, conjI] 3));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   412
by (REPEAT_FIRST (etac conjE));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   413
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   414
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   415
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   416
by (subgoal_tac "? evs'. Xa = Crypt {|Key (newK evs'), Agent Aa|} (serverKey Ba)" 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   417
by (Fast_tac 3);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   418
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   419
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   420
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   421
be subst 5;	(*NS3: discard evsa = Says S Aa... as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   422
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   423
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   424
auto();
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   425
by (ALLGOALS
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   426
    (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,de_Morgan_conj])));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   427
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   428
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   429
by (REPEAT (Safe_step_tac 1));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   430
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   431
qed "Says_Crypt_Nonce_imp_msg_Crypt";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   432
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   433
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   434
 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   435
\               : setOfList evs;  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   436
\           evs : traces                             \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   437
\        |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   438
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   439
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   440
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   441
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   442
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   443
WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   444
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   445
(*If a message is sent, encrypted with a Friend's server key, then either
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   446
  that Friend or the Server originally sent it.*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   447
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   448
 "!!evs. evs : traces ==>                             \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   449
\    ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   450
\        : setOfList evs  -->   \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   451
\    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   452
\            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   453
be traces.induct 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   454
be subst 4;	(*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   455
by (Step_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   456
by (ALLGOALS Asm_full_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   457
(*Remaining cases are Fake, NS2 and NS3*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   458
by (Fast_tac 2);	(*Proves the NS2 case*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   459
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   460
by (REPEAT (dtac spec 2));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   461
fe conjE;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   462
bd mp 2;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   463
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   464
by (REPEAT (resolve_tac [refl, conjI] 2));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   465
by (ALLGOALS Asm_full_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   466
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   467
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   468
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   469
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   470
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   471
be conjE 2;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   472
by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   473
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   474
(*The NS3 case needs the induction hypothesis twice!
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   475
    One application is to the X component of the most recent message.*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   476
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   477
by (Fast_tac 3);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   478
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   479
be conjE 2;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   480
(*DELETE the first quantified formula: it's now useless*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   481
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   482
by (fast_tac (!claset addss (!simpset)) 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   483
(*Now for the Fake case*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   484
be disjE 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   485
(*The subcase of Fake, where the message in question is NOT the most recent*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   486
by (Best_tac 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   487
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   488
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   489
be Crypt_synthesize 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   490
be Key_synthesize 2;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   491
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   492
(*Split up the possibilities of that message being synthesized...*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   493
by (Step_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   494
by (Best_tac 6);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   495
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   496
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   497
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   498
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   499
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   500
 (*The NS3 case needs the induction hypothesis twice!
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   501
    One application is to the X component of the most recent message.*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   502
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   503
????????????????????????????????????????????????????????????????
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   504
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   505
by (Fast_tac 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   506
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   507
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   508
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   509
be conjE 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   510
(*DELETE the first quantified formula: it's now useless*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   511
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   512
by (fast_tac (!claset addss (!simpset)) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   513
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   514
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   515
(*Now for the Fake case*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   516
be disjE 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   517
(*The subcase of Fake, where the message in question is NOT the most recent*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   518
by (Best_tac 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   519
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   520
WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   521
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   522
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   523
Addsimps [new_keys_not_seen];
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   524
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   525
(*Crucial security property: Enemy does not see the keys sent in msg NS2
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   526
   -- even if another friend's key is compromised*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   527
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   528
 "!!evs. [| Says Server (Friend i) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   529
\          (Crypt {|N, Agent B, K, X|} K') : setOfList evs;  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   530
\          evs : traces;  i~=j |] ==> \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   531
\       \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   532
\     K ~: analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   533
be rev_mp 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   534
be traces.induct 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   535
be subst 4;	(*NS2: discard evsa = Says A Server... as irrelevant!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   536
by (ALLGOALS Asm_full_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   537
(*The two simplifications cannot be combined -- they loop!*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   538
by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   539
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   540
br conjI 3;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   541
by (REPEAT_FIRST (resolve_tac [impI]));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   542
by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   543
(*NS1, subgoal concerns "(Says A Server
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   544
                          {|Agent A, Agent B, Nonce (newN evsa)|}"*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   545
(*... thus it cannot equal any components of A's message above.*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   546
by (fast_tac (!claset addss (!simpset)) 2);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   547
(*NS2, the subcase where that message was the most recently sent;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   548
  it holds because here K' = serverKey(Friend i), which Enemies can't see,
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   549
  AND because nobody can know about a brand new key*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   550
by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   551
(*NS2, other subcase.  K is an old key, and thus not in the latest message.*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   552
by (fast_tac 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   553
    (!claset addSEs [less_irrefl]
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   554
             addDs [impOfSubs analyze_insert_Crypt_subset]
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   555
	     addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2);
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   556
(*Now for the Fake case*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   557
be exE 1;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   558
br notI 1;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   559
by (REPEAT (etac conjE 1));
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   560
by (REPEAT (hyp_subst_tac 1));
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   561
by (subgoal_tac 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   562
    "Key (newK evs') : \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   563
\    analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   564
\                                  (sees Enemy evsa))))" 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   565
be (impOfSubs analyze_mono) 2;
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   566
by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   567
			     (2,rev_subsetD),
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   568
			     impOfSubs synthesize_increasing,
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   569
			     impOfSubs analyze_increasing]) 2);
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   570
(*Proves the Fake goal*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   571
by (Auto_tac());
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   572
qed "Enemy_not_see_encrypted_key";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   573
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   574
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   575
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   576
 "!!evs. [| Says Server (Friend i) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   577
\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   578
\           evs : traces;  i~=j    \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   579
\         |] ==> K ~: analyze (sees (Friend j) evs)";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   580
br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   581
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   582
qed "Friend_not_see_encrypted_key";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   583
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   584
goal thy 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   585
 "!!evs. [| Says Server (Friend i) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   586
\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   587
\           A ~: {Friend i, Server};  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   588
\           evs : traces    \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   589
\        |] ==>  K ~: analyze (sees A evs)";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   590
by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   591
by (agent.induct_tac "A" 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   592
by (ALLGOALS Simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   593
by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   594
				     Friend_not_see_encrypted_key]) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   595
br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   596
(*  hyp_subst_tac would deletes the equality assumption... *)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   597
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   598
qed "Agent_not_see_encrypted_key";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   599
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   600
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   601
(*Neatly packaged, perhaps in a useless form*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   602
goalw thy [knownBy_def]
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   603
 "!!evs. [| Says Server (Friend i) \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   604
\             (Crypt {|N, Agent B, K|} K') : setOfList evs;  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   605
\           evs : traces    \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   606
\        |] ==>  knownBy evs K <= {Friend i, Server}";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   607
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   608
by (Step_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   609
br ccontr 1;
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   610
by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   611
qed "knownBy_encrypted_key";
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   612
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   613
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   614
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   615
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   616
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   617
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   618
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   619
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   620
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   621
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   622
goal thy 
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   623
 "!!evs. evs : traces ==> \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   624
\     Says Server A \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   625
\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   626
\     --> (EX evs'. N = Nonce (newN evs'))";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   627
be traces.induct 1;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   628
by (ALLGOALS Asm_simp_tac);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   629
by (Fast_tac 1);
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   630
val Says_Server_lemma = result();
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   631
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   632
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   633
(*NEEDED??*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   634
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   635
goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   636
by (asm_simp_tac (!simpset addsimps [sees_Cons] 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   637
                           setloop split_tac [expand_if]) 1); 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   638
qed "in_sees_Says";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   639
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   640
goal thy "!!A. X ~: parts {Y} ==> \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   641
\              (X : parts (sees A (Says B C Y # evs))) = \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   642
\              (X : parts (sees A evs))";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   643
by (asm_simp_tac (!simpset addsimps [sees_Cons] 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   644
                           setloop split_tac [expand_if]) 1); 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   645
by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   646
qed "in_parts_sees_Says";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   647
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   648
goal thy "!!evs. length evs < length evs' ==> newK  evs ~= newK (A',evs')";
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   649
by (fast_tac (!claset addSEs [less_irrefl]) 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   650
qed "length_less_newK_neq";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   651
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   652
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   653
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   654
goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   655
\         insert {|X,Y|} (insert (Crypt x) evs)";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   656
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   657
qed "insert_Crypt_MPair_delay";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   658
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   659
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   660
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   661
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   662
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   663
goalw thy [keysFor_def]
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   664
    "!!X. Crypt X K: H ==> invKey K : keysFor H";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   665
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   666
qed "keysFor_I";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   667
AddSIs [keysFor_I];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   668
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   669
goalw thy [keysFor_def]
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   670
    "!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   671
by (Fast_tac 1);
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   672
qed "keysFor_D";
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   673
AddSDs [keysFor_D];
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   674
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   675