src/HOL/Auth/Public.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:
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
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    11
(*** Basic properties of pubK & priK ***)
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    12
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    13
AddIffs [inj_pubK RS inj_eq];
3477
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    14
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    15
Goal "(priK A = priK B) = (A=B)";
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
    16
by Safe_tac;
3477
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    17
by (dres_inst_tac [("f","invKey")] arg_cong 1);
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    18
by (Full_simp_tac 1);
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    19
qed "priK_inj_eq";
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    20
3aced7fa7d8b New theorem priK_inj_eq, injectivity of priK
paulson
parents: 3473
diff changeset
    21
AddIffs [priK_inj_eq];
3473
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    22
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
    23
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    24
Goalw [isSymKey_def] "~ isSymKey (pubK A)";
3473
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    25
by (Simp_tac 1);
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    26
qed "not_isSymKey_pubK";
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    27
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    28
Goalw [isSymKey_def] "~ isSymKey (priK A)";
3473
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    29
by (Simp_tac 1);
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    30
qed "not_isSymKey_priK";
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    31
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    32
AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
c2334f9532ab New and stronger lemmas; more default simp/cla rules
paulson
parents: 3465
diff changeset
    33
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    34
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    35
(** "Image" equations that hold for injective functions **)
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    36
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    37
Goal "(invKey x : invKey``A) = (x:A)";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4422
diff changeset
    38
by Auto_tac;
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    39
qed "invKey_image_eq";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    40
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    41
(*holds because invKey is injective*)
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    42
Goal "(pubK x : pubK``A) = (x:A)";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4422
diff changeset
    43
by Auto_tac;
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    44
qed "pubK_image_eq";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    45
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    46
Goal "(priK x ~: pubK``A)";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4422
diff changeset
    47
by Auto_tac;
4422
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    48
qed "priK_pubK_image_eq";
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    49
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
    50
21238c9d363e Simplified proofs using rewrites for f``A where f is injective
paulson
parents: 4091
diff changeset
    51
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    52
(** Rewrites should not refer to  initState(Friend i) 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    53
    -- not in normal form! **)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    54
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    55
Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    56
by (induct_tac "C" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    57
by (auto_tac (claset() addIs [range_eqI], simpset()));
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    58
qed "keysFor_parts_initState";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    59
Addsimps [keysFor_parts_initState];
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    60
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
    61
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    62
(*** Function "spies" ***)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    63
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    64
(*Agents see their own private keys!*)
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    65
Goal "Key (priK A) : initState A";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    66
by (induct_tac "A" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4422
diff changeset
    67
by Auto_tac;
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    68
qed "priK_in_initState";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    69
AddIffs [priK_in_initState];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    70
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    71
(*All public keys are visible*)
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
    72
Goal "Key (pubK A) : spies evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    73
by (induct_tac "evs" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    74
by (ALLGOALS (asm_simp_tac
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5223
diff changeset
    75
	      (simpset() addsimps [imageI, knows_Cons]
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
    76
	                addsplits [expand_event_case])));
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    77
qed_spec_mp "spies_pubK";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    78
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    79
(*Spy sees private keys of bad agents!*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    80
Goal "A: bad ==> Key (priK A) : spies evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
    81
by (induct_tac "evs" 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    82
by (ALLGOALS (asm_simp_tac
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5223
diff changeset
    83
	      (simpset() addsimps [imageI, knows_Cons]
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
    84
	                addsplits [expand_event_case])));
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    85
qed "Spy_spies_bad";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    86
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    87
AddIffs [spies_pubK, spies_pubK RS analz.Inj];
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    88
AddSIs  [Spy_spies_bad];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    89
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    90
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    91
(*For not_bad_tac*)
5114
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    92
Goal "[| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
c729d4c299c1 Deleted leading parameters thanks to new Goal command
paulson
parents: 5076
diff changeset
    93
\           ==> X : analz (spies evs)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    94
by (blast_tac (claset() addSDs [analz.Decrypt]) 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    95
qed "Crypt_Spy_analz_bad";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    96
3442
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
    97
(*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
    98
  a component of a message she's said.*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
    99
fun not_bad_tac s =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   100
    case_tac ("(" ^ s ^ ") : bad") THEN'
3442
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   101
    SELECT_GOAL 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   102
      (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
   103
       REPEAT_DETERM (etac MPair_analz 1) THEN
0b804b390b0e Removed Says_Crypt_lost and Says_Crypt_not_lost.
paulson
parents: 3207
diff changeset
   104
       THEN_BEST_FIRST 
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   105
         (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
   106
         (has_fewer_prems 1, size_of_thm)
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
   107
         Safe_tac);
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   108
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   109
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   110
(*** Fresh nonces ***)
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   111
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   112
Goal "Nonce N ~: parts (initState B)";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
   113
by (induct_tac "B" 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4422
diff changeset
   114
by Auto_tac;
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   115
qed "Nonce_notin_initState";
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   116
AddIffs [Nonce_notin_initState];
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   117
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   118
Goal "Nonce N ~: used []";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   119
by (simp_tac (simpset() addsimps [used_Nil]) 1);
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   120
qed "Nonce_notin_used_empty";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   121
Addsimps [Nonce_notin_used_empty];
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   122
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   123
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   124
(*** 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
   125
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   126
(*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
   127
Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
3667
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3544
diff changeset
   128
by (induct_tac "evs" 1);
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   129
by (res_inst_tac [("x","0")] exI 1);
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   130
by (ALLGOALS (asm_simp_tac
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   131
	      (simpset() addsimps [used_Cons]
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
   132
			addsplits [expand_event_case])));
3730
6933d20f335f Step_tac -> Safe_tac
paulson
parents: 3683
diff changeset
   133
by Safe_tac;
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   134
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   135
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   136
val lemma = result();
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   137
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   138
Goal "EX N. Nonce N ~: used evs";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   139
by (rtac (lemma RS exE) 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   140
by (Blast_tac 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   141
qed "Nonce_supply1";
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3680
diff changeset
   142
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   143
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: 2497
diff changeset
   144
by (rtac (lemma RS exE) 1);
9970
dfe4747c8318 the final renaming: selectI -> someI
paulson
parents: 8054
diff changeset
   145
by (rtac someI 1);
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   146
by (Fast_tac 1);
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   147
qed "Nonce_supply";
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   148
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   149
(*Tactic for possibility theorems*)
3544
6ae62d55a620 Now possibility_tac is an explicit function, in order to delay
paulson
parents: 3519
diff changeset
   150
fun possibility_tac st = st |>
3673
3b06747c3f37 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents: 3667
diff changeset
   151
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
8054
2ce57ef2a4aa used image_eq_UN to speed up slow proofs of base cases
paulson
parents: 6915
diff changeset
   152
    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   153
     THEN
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   154
     REPEAT_FIRST (eq_assume_tac ORELSE' 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
   155
                   resolve_tac [refl, conjI, Nonce_supply]));
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
   156
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   157
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   158
(*** Specialized rewriting for the analz_image_... theorems ***)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   159
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   160
Goal "insert (Key K) H = Key `` {K} Un H";
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   161
by (Blast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   162
qed "insert_Key_singleton";
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   163
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   164
Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   165
by (Blast_tac 1);
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   166
qed "insert_Key_image";
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   167
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3477
diff changeset
   168
(*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
   169
  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
   170
val analz_image_keys_ss = 
6915
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6308
diff changeset
   171
     simpset() delsimps [image_insert, image_Un]
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6308
diff changeset
   172
	       delsimps [imp_disjL]    (*reduces blow-up*)
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6308
diff changeset
   173
	       addsimps [image_insert RS sym, image_Un RS sym,
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6308
diff changeset
   174
			 rangeI, 
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6308
diff changeset
   175
			 insert_Key_singleton, 
4ab8e31a8421 Now if_weak_cong is a standard congruence rule
paulson
parents: 6308
diff changeset
   176
			 insert_Key_image, Un_assoc RS sym];
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
   177