src/HOL/Auth/Public.ML
author paulson
Tue, 16 Dec 1997 15:17:26 +0100
changeset 4422 21238c9d363e
parent 4091 771b1f6422a8
child 4477 b3e5857d8d99
permissions -rw-r--r--
Simplified proofs using rewrites for f``A where f is injective
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Public
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     2
    ID:         $Id$
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     5
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     6
Theory of Public Keys (common to all symmetric-key protocols)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     7
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     9
*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    10
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    11
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    12
open Public;
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    13
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    14
(*** Basic properties of pubK & priK ***)
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    15
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    16
AddIffs [inj_pubK RS inj_eq];
3477
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    17
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    18
goal thy "!!A B. (priK A = priK B) = (A=B)";
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
    19
by Safe_tac;
3477
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    20
by (dres_inst_tac [("f","invKey")] arg_cong 1);
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    21
by (Full_simp_tac 1);
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    22
qed "priK_inj_eq";
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    23
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    24
AddIffs [priK_inj_eq];
3473
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    25
AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    26
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    27
goalw thy [isSymKey_def] "~ isSymKey (pubK A)";
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    28
by (Simp_tac 1);
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    29
qed "not_isSymKey_pubK";
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    30
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    31
goalw thy [isSymKey_def] "~ isSymKey (priK A)";
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    32
by (Simp_tac 1);
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    33
qed "not_isSymKey_priK";
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    34
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    35
AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    36
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    37
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    38
(** "Image" equations that hold for injective functions **)
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    39
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    40
goal thy "(invKey x : invKey``A) = (x:A)";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    41
by (Auto_tac());
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    42
qed "invKey_image_eq";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    43
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    44
(*holds because invKey is injective*)
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    45
goal thy "(pubK x : pubK``A) = (x:A)";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    46
by (Auto_tac());
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    47
qed "pubK_image_eq";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    48
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    49
goal thy "(priK x ~: pubK``A)";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    50
by (Auto_tac());
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    51
qed "priK_pubK_image_eq";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    52
Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    53
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    54
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    55
(** Rewrites should not refer to  initState(Friend i) 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    56
    -- not in normal form! **)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    57
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    58
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    59
by (induct_tac "C" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    60
by (auto_tac (claset() addIs [range_eqI], simpset()));
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    61
qed "keysFor_parts_initState";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    62
Addsimps [keysFor_parts_initState];
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    63
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    64
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    65
(*** Function "spies" ***)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    66
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    67
(*Agents see their own private keys!*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    68
goal thy "Key (priK A) : initState A";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    69
by (induct_tac "A" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    70
by (Auto_tac());
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    71
qed "priK_in_initState";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    72
AddIffs [priK_in_initState];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    73
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    74
(*All public keys are visible*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    75
goal thy "Key (pubK A) : spies evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    76
by (induct_tac "evs" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    77
by (ALLGOALS (asm_simp_tac
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    78
	      (simpset() addsimps [imageI, spies_Cons]
3919
c036caebfc75 setloop split_tac -> addsplits
nipkow
parents: 3730
diff changeset
    79
	                addsplits [expand_event_case, expand_if])));
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    80
qed_spec_mp "spies_pubK";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    81
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    82
(*Spy sees private keys of bad agents!*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    83
goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    84
by (induct_tac "evs" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    85
by (ALLGOALS (asm_simp_tac
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    86
	      (simpset() addsimps [imageI, spies_Cons]
3919
c036caebfc75 setloop split_tac -> addsplits
nipkow
parents: 3730
diff changeset
    87
	                addsplits [expand_event_case, expand_if])));
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    88
qed "Spy_spies_bad";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    89
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    90
AddIffs [spies_pubK, spies_pubK RS analz.Inj];
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    91
AddSIs  [Spy_spies_bad];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    92
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    93
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    94
(*For not_bad_tac*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    95
goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    96
\              ==> X : analz (spies evs)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    97
by (blast_tac (claset() addSDs [analz.Decrypt]) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    98
qed "Crypt_Spy_analz_bad";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    99
3442
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   100
(*Prove that the agent is uncompromised by the confidentiality of 
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   101
  a component of a message she's said.*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   102
fun not_bad_tac s =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   103
    case_tac ("(" ^ s ^ ") : bad") THEN'
3442
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   104
    SELECT_GOAL 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   105
      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
3442
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   106
       REPEAT_DETERM (etac MPair_analz 1) THEN
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   107
       THEN_BEST_FIRST 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   108
         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
3442
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   109
         (has_fewer_prems 1, size_of_thm)
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
   110
         Safe_tac);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   111
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   112
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   113
(*** Fresh nonces ***)
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   114
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
   115
goal thy "Nonce N ~: parts (initState B)";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
   116
by (induct_tac "B" 1);
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   117
by (Auto_tac ());
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   118
qed "Nonce_notin_initState";
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   119
AddIffs [Nonce_notin_initState];
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   120
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   121
goal thy "Nonce N ~: used []";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   122
by (simp_tac (simpset() addsimps [used_Nil]) 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   123
qed "Nonce_notin_used_empty";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   124
Addsimps [Nonce_notin_used_empty];
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   125
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   126
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   127
(*** Supply fresh nonces for possibility theorems. ***)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   128
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   129
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   130
goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
   131
by (induct_tac "evs" 1);
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   132
by (res_inst_tac [("x","0")] exI 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   133
by (ALLGOALS (asm_simp_tac
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   134
	      (simpset() addsimps [used_Cons]
3919
c036caebfc75 setloop split_tac -> addsplits
nipkow
parents: 3730
diff changeset
   135
			addsplits [expand_event_case, expand_if])));
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
   136
by Safe_tac;
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   137
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   138
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   139
val lemma = result();
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   140
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   141
goal thy "EX N. Nonce N ~: used evs";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   142
by (rtac (lemma RS exE) 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   143
by (Blast_tac 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   144
qed "Nonce_supply1";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   145
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   146
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   147
by (rtac (lemma RS exE) 1);
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   148
by (rtac selectI 1);
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   149
by (Fast_tac 1);
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   150
qed "Nonce_supply";
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   151
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   152
(*Tactic for possibility theorems*)
3544
6ae62d55a620 Now possibility_tac is an explicit function, in order to delay
paulson
parents: 3519
diff changeset
   153
fun possibility_tac st = st |>
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   154
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   155
    (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: 2497
diff changeset
   156
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   157
     REPEAT_FIRST (eq_assume_tac ORELSE' 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   158
                   resolve_tac [refl, conjI, Nonce_supply]));
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   159
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   160
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   161
(*** Specialized rewriting for the analz_image_... theorems ***)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   162
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   163
goal thy "insert (Key K) H = Key `` {K} Un H";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   164
by (Blast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   165
qed "insert_Key_singleton";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   166
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   167
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   168
by (Blast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   169
qed "insert_Key_image";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   170
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   171
(*Reverse the normal simplification of "image" to build up (not break down)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   172
  the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   173
val analz_image_keys_ss = 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   174
     simpset() addcongs [if_weak_cong]
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   175
	      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
   176
              delsimps [imp_disjL]    (*reduces blow-up*)
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   177
              addsimps [image_insert RS sym, image_Un RS sym,
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   178
			rangeI, 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   179
			insert_Key_singleton, 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   180
			insert_Key_image, Un_assoc RS sym]
3919
c036caebfc75 setloop split_tac -> addsplits
nipkow
parents: 3730
diff changeset
   181
              addsplits [expand_if];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   182