src/HOL/Auth/Shared.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9970 dfe4747c8318
child 10833 c0844a30ea4e
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    11
(*** Basic properties of shrK ***)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    13
(*Injectiveness: Agents' long-term keys are distinct.*)
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    14
AddIffs [inj_shrK RS inj_eq];
2376
f5c61fd9b9b6 Temporary additions (random) for the nested Otway-Rees protocol
paulson
parents: 2320
diff changeset
    15
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    16
(* invKey(shrK A) = shrK A *)
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
    17
Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
2320
41289907faed Moved much common material to Message.ML
paulson
parents: 2284
diff changeset
    18
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    19
(** Rewrites should not refer to  initState(Friend i) 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    20
    -- not in normal form! **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    21
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    22
Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
    23
by (induct_tac "C" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
    24
by Auto_tac;
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    25
qed "keysFor_parts_initState";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    26
Addsimps [keysFor_parts_initState];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    27
4509
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
    28
(*Specialized to shared-key model: no need for addss in protocol proofs*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    29
Goal "[| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
4509
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
    30
\              ==> K : keysFor (parts H) | Key K : parts H";
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    31
by (force_tac
4509
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
    32
      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
    33
			impOfSubs (analz_subset_parts RS keysFor_mono)]
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    34
		addIs  [impOfSubs analz_subset_parts],
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    35
       simpset()) 1);
4509
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
    36
qed "keysFor_parts_insert";
828148415197 Making proofs faster, especially using keysFor_parts_insert
paulson
parents: 4477
diff changeset
    37
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    38
Goal "Crypt K X : H ==> K : keysFor H";
4238
679a233fb206 Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents: 4156
diff changeset
    39
by (dtac Crypt_imp_invKey_keysFor 1);
679a233fb206 Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents: 4156
diff changeset
    40
by (Asm_full_simp_tac 1);
679a233fb206 Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents: 4156
diff changeset
    41
qed "Crypt_imp_keysFor";
679a233fb206 Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents: 4156
diff changeset
    42
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    43
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    44
(*** Function "knows" ***)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    45
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    46
(*Spy sees shared keys of agents!*)
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    47
Goal "A: bad ==> Key (shrK A) : knows Spy evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
    48
by (induct_tac "evs" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    49
by (ALLGOALS (asm_simp_tac
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    50
	      (simpset() addsimps [imageI, knows_Cons]
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4633
diff changeset
    51
	                addsplits [expand_event_case])));
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    52
qed "Spy_knows_Spy_bad";
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    53
AddSIs [Spy_knows_Spy_bad];
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    54
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    55
(*For not_bad_tac*)
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    56
Goal "[| Crypt (shrK A) X : analz (knows Spy evs);  A: bad |] \
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    57
\              ==> X : analz (knows Spy evs)";
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
    58
by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    59
qed "Crypt_Spy_analz_bad";
2072
6ac12b9478d5 Put in the theorem Says_Crypt_not_lost
paulson
parents: 2064
diff changeset
    60
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    61
(*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
    62
  a component of a message she's said.*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    63
fun not_bad_tac s =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    64
    case_tac ("(" ^ s ^ ") : bad") THEN'
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    65
    SELECT_GOAL 
6334
e53457213857 updated not_bad_tac for the Gets model
paulson
parents: 6308
diff changeset
    66
      (REPEAT_DETERM (etac exE 1) THEN
e53457213857 updated not_bad_tac for the Gets model
paulson
parents: 6308
diff changeset
    67
       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
    68
       REPEAT_DETERM (etac MPair_analz 1) THEN
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    69
       THEN_BEST_FIRST 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    70
         (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
    71
         (has_fewer_prems 1, size_of_thm)
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    72
         (Step_tac 1));
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    73
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    74
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    75
(** 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
    76
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    77
(*Agents see their own shared keys!*)
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    78
Goal "Key (shrK A) : initState A";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    79
by (induct_tac "A" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
    80
by Auto_tac;
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    81
qed "shrK_in_initState";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    82
AddIffs [shrK_in_initState];
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    83
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    84
Goal "Key (shrK A) : used evs";
4423
a129b817b58a expandshort;
wenzelm
parents: 4369
diff changeset
    85
by (rtac initState_into_used 1);
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
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_in_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    88
AddIffs [shrK_in_used];
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    89
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    90
(*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
    91
  from long-term shared keys*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    92
Goal "Key K ~: used evs ==> K ~: range shrK";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    93
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    94
qed "Key_not_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    95
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    96
Goal "Key K ~: used evs ==> shrK B ~= K";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    97
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    98
qed "shrK_neq";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    99
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   100
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
3961
6a8996fb7d99 Many minor speedups:
paulson
parents: 3919
diff changeset
   101
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   102
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   103
(*** Fresh nonces ***)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   104
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   105
Goal "Nonce N ~: parts (initState B)";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
   106
by (induct_tac "B" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   107
by Auto_tac;
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   108
qed "Nonce_notin_initState";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   109
AddIffs [Nonce_notin_initState];
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   110
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   111
Goal "Nonce N ~: used []";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   112
by (simp_tac (simpset() addsimps [used_Nil]) 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   113
qed "Nonce_notin_used_empty";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   114
Addsimps [Nonce_notin_used_empty];
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   115
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   116
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   117
(*** Supply fresh nonces for possibility theorems. ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   118
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   119
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   120
Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3542
diff changeset
   121
by (induct_tac "evs" 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   122
by (res_inst_tac [("x","0")] exI 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   123
by (ALLGOALS (asm_simp_tac
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   124
	      (simpset() addsimps [used_Cons]
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4633
diff changeset
   125
			addsplits [expand_event_case])));
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3708
diff changeset
   126
by Safe_tac;
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   127
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   128
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
   129
val lemma = result();
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   130
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   131
Goal "EX N. Nonce N ~: used evs";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   132
by (rtac (lemma RS exE) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   133
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   134
qed "Nonce_supply1";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   135
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   136
Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   137
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
   138
by (cut_inst_tac [("evs","evs'")] lemma 1);
3708
56facaebf3e3 Changed some proofs to use Clarify_tac
paulson
parents: 3683
diff changeset
   139
by (Clarify_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   140
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
   141
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
5502
da4d0444ea85 new theorem less_Suc_eq_le
paulson
parents: 5492
diff changeset
   142
by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
da4d0444ea85 new theorem less_Suc_eq_le
paulson
parents: 5492
diff changeset
   143
				      less_Suc_eq_le]) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   144
qed "Nonce_supply2";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   145
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   146
Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   147
\                   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
   148
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
   149
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
   150
by (cut_inst_tac [("evs","evs''")] lemma 1);
3708
56facaebf3e3 Changed some proofs to use Clarify_tac
paulson
parents: 3683
diff changeset
   151
by (Clarify_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   152
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
   153
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
   154
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
5502
da4d0444ea85 new theorem less_Suc_eq_le
paulson
parents: 5492
diff changeset
   155
by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
da4d0444ea85 new theorem less_Suc_eq_le
paulson
parents: 5492
diff changeset
   156
				      less_Suc_eq_le]) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   157
qed "Nonce_supply3";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   158
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   159
Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   160
by (rtac (lemma RS exE) 1);
9970
dfe4747c8318 the final renaming: selectI -> someI
paulson
parents: 6915
diff changeset
   161
by (rtac someI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   162
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   163
qed "Nonce_supply";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   164
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   165
(*** Supply fresh keys for possibility theorems. ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   166
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   167
Goal "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
   168
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   169
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   170
qed "Key_supply1";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   171
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   172
Goal "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
   173
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
   174
by (etac exE 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   175
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
   176
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
4633
d4a074973715 corrected problem with auto_tac: now uses a variant of depth_tac that avoids
oheimb
parents: 4509
diff changeset
   177
by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   178
qed "Key_supply2";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   179
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   180
Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   181
\                      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
   182
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
   183
by (etac exE 1);
4156
31251763848d Tidied Key_supply3
paulson
parents: 4091
diff changeset
   184
(*Blast_tac requires instantiation of the keys for some reason*)
31251763848d Tidied Key_supply3
paulson
parents: 4091
diff changeset
   185
by (cut_inst_tac [("evs","evs'"), ("a1","K")] 
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   186
    (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
   187
by (etac exE 1);
4156
31251763848d Tidied Key_supply3
paulson
parents: 4091
diff changeset
   188
by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] 
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 3207
diff changeset
   189
    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
4156
31251763848d Tidied Key_supply3
paulson
parents: 4091
diff changeset
   190
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   191
qed "Key_supply3";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   192
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   193
Goal "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
   194
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
9970
dfe4747c8318 the final renaming: selectI -> someI
paulson
parents: 6915
diff changeset
   195
by (rtac someI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   196
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   197
qed "Key_supply";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   198
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   199
(*** Tactics for possibility theorems ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   200
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   201
(*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
   202
    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
   203
fun possibility_tac st = st |>
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   204
   (REPEAT 
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
   205
    (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5535
diff changeset
   206
                         setSolver safe_solver))
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   207
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   208
     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
   209
                   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
   210
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   211
(*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
   212
  nonces and keys initially*)
3542
db5e9aceea49 Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents: 3519
diff changeset
   213
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
   214
    REPEAT 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   215
    (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
   216
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   217
     REPEAT_FIRST (resolve_tac [refl, conjI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   218
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   219
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
   220
(*** Specialized rewriting for analz_insert_freshK ***)
2320
41289907faed Moved much common material to Message.ML
paulson
parents: 2284
diff changeset
   221
5492
d9fc3457554e From Compl(A) to -A
paulson
parents: 5351
diff changeset
   222
Goal "A <= - (range shrK) ==> shrK x ~: A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   223
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   224
qed "subset_Compl_range";
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   225
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   226
Goal "insert (Key K) H = Key `` {K} Un H";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   227
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   228
qed "insert_Key_singleton";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   229
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   230
Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   231
by (Blast_tac 1);
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   232
qed "insert_Key_image";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   233
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3443
diff changeset
   234
(*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
   235
  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
   236
  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
   237
val analz_image_freshK_ss = 
6915
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   238
     simpset() delsimps [image_insert, image_Un]
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   239
	       delsimps [imp_disjL]    (*reduces blow-up*)
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   240
	       addsimps [image_insert RS sym, image_Un RS sym,
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   241
			 analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   242
			 insert_Key_singleton, subset_Compl_range,
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   243
			 Key_not_used, insert_Key_image, Un_assoc RS sym]
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6334
diff changeset
   244
			@disj_comms;
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   245
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   246
(*Lemma for the trivial direction of the if-and-only-if*)
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5223
diff changeset
   247
Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   248
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3961
diff changeset
   249
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
   250
qed "analz_image_freshK_lemma";