src/HOL/Auth/Shared.ML
author paulson
Mon, 29 Sep 1997 11:47:01 +0200
changeset 3730 6933d20f335f
parent 3708 56facaebf3e3
child 3908 4f19a40a9343
permissions -rw-r--r--
Step_tac -> Safe_tac
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2320
41289907faed Moved much common material to Message.ML
paulson
parents: 2284
diff changeset
     1
(*  Title:      HOL/Auth/Shared
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
     8
Shared, long-term keys; initial states of agents
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
     9
*)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    10
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    11
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
open Shared;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    13
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    14
(*** Basic properties of shrK ***)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    15
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    16
(*Injectiveness: Agents' long-term keys are distinct.*)
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    17
AddIffs [inj_shrK RS inj_eq];
2376
f5c61fd9b9b6 Temporary additions (random) for the nested Otway-Rees protocol
paulson
parents: 2320
diff changeset
    18
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    19
(* invKey(shrK A) = shrK A *)
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    20
Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
2320
41289907faed Moved much common material to Message.ML
paulson
parents: 2284
diff changeset
    21
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    22
(** Rewrites should not refer to  initState(Friend i) 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    23
    -- not in normal form! **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    24
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    25
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
    26
by (induct_tac "C" 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    27
by (Auto_tac ());
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    28
qed "keysFor_parts_initState";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    29
Addsimps [keysFor_parts_initState];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    30
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    31
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    32
(*** Function "spies" ***)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    33
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    34
(*Spy sees shared keys of agents!*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    35
goal thy "!!A. A: bad ==> Key (shrK A) : spies evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
    36
by (induct_tac "evs" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    37
by (ALLGOALS (asm_simp_tac
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    38
	      (!simpset addsimps [imageI, spies_Cons]
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    39
	                setloop split_tac [expand_event_case, expand_if])));
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    40
qed "Spy_spies_bad";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    41
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    42
AddSIs [Spy_spies_bad];
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    43
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    44
(*For not_bad_tac*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    45
goal thy "!!A. [| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    46
\              ==> X : analz (spies evs)";
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    47
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    48
qed "Crypt_Spy_analz_bad";
2072
6ac12b9478d5 Put in the theorem Says_Crypt_not_lost
paulson
parents: 2064
diff changeset
    49
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    50
(*Prove that the agent is uncompromised by the confidentiality of 
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    51
  a component of a message she's said.*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    52
fun not_bad_tac s =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    53
    case_tac ("(" ^ s ^ ") : bad") THEN'
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    54
    SELECT_GOAL 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    55
      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    56
       REPEAT_DETERM (etac MPair_analz 1) THEN
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    57
       THEN_BEST_FIRST 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    58
         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    59
         (has_fewer_prems 1, size_of_thm)
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    60
         (Step_tac 1));
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    61
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    62
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    63
(** Fresh keys never clash with long-term shared keys **)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    64
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    65
(*Agents see their own shared keys!*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    66
goal thy "Key (shrK A) : initState A";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    67
by (induct_tac "A" 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    68
by (Auto_tac());
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    69
qed "shrK_in_initState";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    70
AddIffs [shrK_in_initState];
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    71
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    72
goal thy "Key (shrK A) : used evs";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    73
br initState_into_used 1;
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    74
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    75
qed "shrK_in_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    76
AddIffs [shrK_in_used];
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    77
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    78
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    79
  from long-term shared keys*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    80
goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    81
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    82
qed "Key_not_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    83
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    84
(*A session key cannot clash with a long-term shared key*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    85
goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    86
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    87
qed "shrK_neq";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    88
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    89
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    90
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    91
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    92
(*** Fresh nonces ***)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    93
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    94
goal thy "Nonce N ~: parts (initState B)";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
    95
by (induct_tac "B" 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    96
by (Auto_tac ());
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    97
qed "Nonce_notin_initState";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    98
AddIffs [Nonce_notin_initState];
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    99
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   100
goal thy "Nonce N ~: used []";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   101
by (simp_tac (!simpset addsimps [used_Nil]) 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   102
qed "Nonce_notin_used_empty";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   103
Addsimps [Nonce_notin_used_empty];
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   104
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   105
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   106
(*** Supply fresh nonces for possibility theorems. ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   107
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   108
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   109
goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
   110
by (induct_tac "evs" 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   111
by (res_inst_tac [("x","0")] exI 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   112
by (ALLGOALS (asm_simp_tac
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   113
	      (!simpset addsimps [used_Cons]
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   114
			setloop split_tac [expand_event_case, expand_if])));
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3708
diff changeset
   115
by Safe_tac;
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   116
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   117
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   118
val lemma = result();
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   119
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   120
goal thy "EX N. Nonce N ~: used evs";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   121
by (rtac (lemma RS exE) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   122
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   123
qed "Nonce_supply1";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   124
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   125
goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   126
by (cut_inst_tac [("evs","evs")] lemma 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   127
by (cut_inst_tac [("evs","evs'")] lemma 1);
3708
56facaebf3e3 Changed some proofs to use Clarify_tac
paulson
parents: 3683
diff changeset
   128
by (Clarify_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   129
by (res_inst_tac [("x","N")] exI 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   130
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   131
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   132
				     le_add2, le_add1, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   133
				     le_eq_less_Suc RS sym]) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   134
qed "Nonce_supply2";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   135
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   136
goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   137
\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   138
by (cut_inst_tac [("evs","evs")] lemma 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   139
by (cut_inst_tac [("evs","evs'")] lemma 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   140
by (cut_inst_tac [("evs","evs''")] lemma 1);
3708
56facaebf3e3 Changed some proofs to use Clarify_tac
paulson
parents: 3683
diff changeset
   141
by (Clarify_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   142
by (res_inst_tac [("x","N")] exI 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   143
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   144
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   145
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   146
				     le_add2, le_add1, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   147
				     le_eq_less_Suc RS sym]) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   148
by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   149
by (stac (le_eq_less_Suc RS sym) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   150
by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   151
by (REPEAT (rtac le_add1 1));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   152
qed "Nonce_supply3";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   153
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   154
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   155
by (rtac (lemma RS exE) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   156
by (rtac selectI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   157
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   158
qed "Nonce_supply";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   159
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   160
(*** Supply fresh keys for possibility theorems. ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   161
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   162
goal thy "EX K. Key K ~: used evs";
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   163
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   164
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   165
qed "Key_supply1";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   166
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   167
goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   168
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   169
by (etac exE 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   170
by (cut_inst_tac [("evs","evs'")] 
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   171
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   172
by (Auto_tac());
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   173
qed "Key_supply2";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   174
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   175
goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   176
\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   177
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   178
by (etac exE 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   179
by (cut_inst_tac [("evs","evs'")] 
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   180
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   181
by (etac exE 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   182
by (cut_inst_tac [("evs","evs''")] 
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   183
    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
3708
56facaebf3e3 Changed some proofs to use Clarify_tac
paulson
parents: 3683
diff changeset
   184
by (Clarify_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   185
by (Full_simp_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   186
by (fast_tac (!claset addSEs [allE]) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   187
qed "Key_supply3";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   188
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   189
goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   190
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   191
by (rtac selectI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   192
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   193
qed "Key_supply";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   194
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   195
(*** Tactics for possibility theorems ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   196
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   197
(*Omitting used_Says makes the tactic much faster: it leaves expressions
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   198
    such as  Nonce ?N ~: used evs that match Nonce_supply*)
3542
db5e9aceea49 Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents: 3519
diff changeset
   199
fun possibility_tac st = st |>
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   200
   (REPEAT 
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   201
    (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver))
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   202
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   203
     REPEAT_FIRST (eq_assume_tac ORELSE' 
3542
db5e9aceea49 Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents: 3519
diff changeset
   204
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   205
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   206
(*For harder protocols (such as Recur) where we have to set up some
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   207
  nonces and keys initially*)
3542
db5e9aceea49 Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents: 3519
diff changeset
   208
fun basic_possibility_tac st = st |>
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   209
    REPEAT 
2637
e9b203f854ae reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents: 2516
diff changeset
   210
    (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   211
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   212
     REPEAT_FIRST (resolve_tac [refl, conjI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   213
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   214
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
   215
(*** Specialized rewriting for analz_insert_freshK ***)
2320
41289907faed Moved much common material to Message.ML
paulson
parents: 2284
diff changeset
   216
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   217
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   218
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   219
qed "subset_Compl_range";
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   220
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   221
goal thy "insert (Key K) H = Key `` {K} Un H";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   222
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   223
qed "insert_Key_singleton";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   224
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   225
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   226
by (Blast_tac 1);
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   227
qed "insert_Key_image";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   228
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3443
diff changeset
   229
(*Reverse the normal simplification of "image" to build up (not break down)
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3443
diff changeset
   230
  the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3443
diff changeset
   231
  erase occurrences of forwarded message components (X).*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   232
val analz_image_freshK_ss = 
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   233
     !simpset addcongs [if_weak_cong]
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   234
	      delsimps [image_insert, image_Un]
3680
7588653475b2 Removed the simprule imp_disjL from the analz_image_..._ss to boost speed
paulson
parents: 3673
diff changeset
   235
              delsimps [imp_disjL]    (*reduces blow-up*)
3479
2aacd6f10654 Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents: 3472
diff changeset
   236
              addsimps ([image_insert RS sym, image_Un RS sym,
2aacd6f10654 Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents: 3472
diff changeset
   237
                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   238
                         insert_Key_singleton, subset_Compl_range,
3479
2aacd6f10654 Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents: 3472
diff changeset
   239
                         Key_not_used, insert_Key_image, Un_assoc RS sym]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   240
                        @disj_comms)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   241
              setloop split_tac [expand_if];
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   242
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   243
(*Lemma for the trivial direction of the if-and-only-if*)
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   244
goal thy  
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   245
 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   246
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
2922
580647a879cf Using Blast_tac
paulson
parents: 2891
diff changeset
   247
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   248
qed "analz_image_freshK_lemma";