src/HOL/Auth/Shared.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3479 2aacd6f10654
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    25
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    26
by (agent.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
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    32
(*** Function "sees" ***)
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    33
1964
d551e68b7a36 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    34
(*Agents see their own shared keys!*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    35
goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    36
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    37
by (agent.induct_tac "A" 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    38
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    39
by (Blast_tac 1);
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    40
qed_spec_mp "sees_own_shrK";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    41
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    42
(*Spy sees shared keys of lost agents!*)
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
    43
goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs";
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    44
by (list.induct_tac "evs" 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    45
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    46
by (Blast_tac 1);
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
    47
qed "Spy_sees_lost";
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    48
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
    49
AddSIs [sees_own_shrK, Spy_sees_lost];
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2026
diff changeset
    50
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    51
(*For not_lost_tac*)
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    52
goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs);  A: lost |] \
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    53
\              ==> X : analz (sees lost Spy evs)";
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    54
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    55
qed "Crypt_Spy_analz_lost";
2072
6ac12b9478d5 Put in the theorem Says_Crypt_not_lost
paulson
parents: 2064
diff changeset
    56
3443
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    57
(*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
    58
  a component of a message she's said.*)
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    59
fun not_lost_tac s =
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    60
    case_tac ("(" ^ s ^ ") : lost") THEN'
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    61
    SELECT_GOAL 
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    62
      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    63
       REPEAT_DETERM (etac MPair_analz 1) THEN
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    64
       THEN_BEST_FIRST 
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    65
         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    66
         (has_fewer_prems 1, size_of_thm)
387ca417e7f5 Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3414
diff changeset
    67
         (Step_tac 1));
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    68
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    69
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    70
(** 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
    71
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";
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    73
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    74
qed "shrK_in_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    75
AddIffs [shrK_in_used];
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    76
3121
cbb6c0c1c58a Conversion to use blast_tac (with other improvements)
paulson
parents: 2922
diff changeset
    77
(*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
    78
  from long-term shared keys*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    79
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
    80
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    81
qed "Key_not_used";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    82
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    83
(*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
    84
goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    85
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    86
qed "shrK_neq";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    87
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    88
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
    89
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    90
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    91
(*** Fresh nonces ***)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    92
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    93
goal thy "Nonce N ~: parts (initState lost B)";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    94
by (agent.induct_tac "B" 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    95
by (Auto_tac ());
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    96
qed "Nonce_notin_initState";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    97
AddIffs [Nonce_notin_initState];
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    98
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
    99
goal thy "Nonce N ~: used []";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   100
by (simp_tac (!simpset addsimps [used_def]) 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   101
qed "Nonce_notin_used_empty";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   102
Addsimps [Nonce_notin_used_empty];
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   103
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
(*** Supply fresh nonces for possibility theorems. ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   106
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   107
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   108
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   109
by (list.induct_tac "evs" 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   110
by (res_inst_tac [("x","0")] exI 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   111
by (Step_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   112
by (Full_simp_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   113
(*Inductive step*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   114
by (event.induct_tac "a" 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   115
by (ALLGOALS (full_simp_tac 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   116
	      (!simpset delsimps [sees_Notes]
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   117
		        addsimps [UN_parts_sees_Says,
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   118
				  UN_parts_sees_Notes])));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   119
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   120
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
   121
val lemma = result();
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   122
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   123
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
   124
by (rtac (lemma RS exE) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   125
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   126
qed "Nonce_supply1";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   127
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   128
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
   129
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
   130
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
   131
by (Step_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   132
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
   133
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
   134
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
   135
				     le_add2, le_add1, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   136
				     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
   137
qed "Nonce_supply2";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   138
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   139
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
   140
\                   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
   141
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
   142
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
   143
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
   144
by (Step_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   145
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
   146
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
   147
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
   148
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
   149
				     le_add2, le_add1, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   150
				     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
   151
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
   152
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
   153
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
   154
by (REPEAT (rtac le_add1 1));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   155
qed "Nonce_supply3";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   156
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   157
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
   158
by (rtac (lemma RS exE) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   159
by (rtac selectI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   160
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   161
qed "Nonce_supply";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   162
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   163
(*** Supply fresh keys for possibility theorems. ***)
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
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
   166
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   167
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   168
qed "Key_supply1";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   169
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   170
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
   171
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
   172
by (etac exE 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   173
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
   174
    (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
   175
by (Auto_tac());
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   176
qed "Key_supply2";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   177
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   178
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
   179
\                      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
   180
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
   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 Key_supply_ax) 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   184
by (etac exE 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   185
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
   186
    (Finites.emptyI RS Finites.insertI 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 (Step_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   188
by (Full_simp_tac 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   189
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
   190
qed "Key_supply3";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   191
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   192
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
   193
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
   194
by (rtac selectI 1);
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   195
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   196
qed "Key_supply";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   197
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   198
(*** Tactics for possibility theorems ***)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   199
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   200
val possibility_tac =
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   201
    REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3479
diff changeset
   202
    (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
   203
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   204
     REPEAT_FIRST (eq_assume_tac ORELSE' 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   205
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   206
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   207
(*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
   208
  nonces and keys initially*)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   209
val basic_possibility_tac =
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   210
    REPEAT 
2637
e9b203f854ae reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents: 2516
diff changeset
   211
    (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
   212
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   213
     REPEAT_FIRST (resolve_tac [refl, conjI]));
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   214
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   215
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3465
diff changeset
   216
(*** Specialized rewriting for analz_insert_freshK ***)
2320
41289907faed Moved much common material to Message.ML
paulson
parents: 2284
diff changeset
   217
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   218
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   219
by (Blast_tac 1);
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   220
qed "subset_Compl_range";
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   221
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   222
goal thy "insert (Key K) H = Key `` {K} Un H";
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 "insert_Key_singleton";
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   225
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   226
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
   227
by (Blast_tac 1);
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   228
qed "insert_Key_image";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   229
3451
d10f100676d8 Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents: 3443
diff changeset
   230
(*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
   231
  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
   232
  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
   233
val analz_image_freshK_ss = 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   234
     !simpset delsimps [image_insert, image_Un]
3479
2aacd6f10654 Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents: 3472
diff changeset
   235
              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
   236
                         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
   237
                         insert_Key_singleton, subset_Compl_range,
3479
2aacd6f10654 Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents: 3472
diff changeset
   238
                         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
   239
                        @disj_comms)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
   240
              setloop split_tac [expand_if];
2045
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   241
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   242
(*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
   243
goal thy  
ae1030e66745 Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents: 2032
diff changeset
   244
 "!!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
   245
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
2922
580647a879cf Using Blast_tac
paulson
parents: 2891
diff changeset
   246
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
   247
qed "analz_image_freshK_lemma";