author | paulson |
Tue, 24 Apr 2001 12:19:01 +0200 | |
changeset 11264 | a47a9288f3f6 |
parent 11251 | a6816d47f41d |
child 11270 | a315a3862bb4 |
permissions | -rw-r--r-- |
1839 | 1 |
(* Title: HOL/Auth/Message |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Datatypes of agents and messages; |
|
1913 | 7 |
Inductive relations "parts", "analz" and "synth" |
1839 | 8 |
*) |
9 |
||
11189 | 10 |
theory Message = Main |
11 |
files ("Message_lemmas.ML"): |
|
12 |
||
13 |
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
|
14 |
lemma [simp] : "A Un (B Un A) = B Un A" |
|
15 |
by blast |
|
1839 | 16 |
|
17 |
types |
|
18 |
key = nat |
|
19 |
||
20 |
consts |
|
11189 | 21 |
invKey :: "key=>key" |
1839 | 22 |
|
11189 | 23 |
axioms |
24 |
invKey [simp] : "invKey (invKey K) = K" |
|
1839 | 25 |
|
26 |
(*The inverse of a symmetric key is itself; |
|
27 |
that of a public key is the private key and vice versa*) |
|
28 |
||
29 |
constdefs |
|
11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11192
diff
changeset
|
30 |
symKeys :: "key set" |
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11192
diff
changeset
|
31 |
"symKeys == {K. invKey K = K}" |
1839 | 32 |
|
33 |
datatype (*We allow any number of friendly agents*) |
|
2032 | 34 |
agent = Server | Friend nat | Spy |
1839 | 35 |
|
3668 | 36 |
datatype |
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset
|
37 |
msg = Agent agent (*Agent names*) |
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset
|
38 |
| Number nat (*Ordinary integers, timestamps, ...*) |
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset
|
39 |
| Nonce nat (*Unguessable nonces*) |
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset
|
40 |
| Key key (*Crypto keys*) |
5234 | 41 |
| Hash msg (*Hashing*) |
42 |
| MPair msg msg (*Compound messages*) |
|
43 |
| Crypt key msg (*Encryption, public- or shared-key*) |
|
1839 | 44 |
|
5234 | 45 |
|
46 |
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) |
|
47 |
syntax |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset
|
48 |
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
1839 | 49 |
|
9686 | 50 |
syntax (xsymbols) |
11189 | 51 |
"@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
9686 | 52 |
|
1839 | 53 |
translations |
54 |
"{|x, y, z|}" == "{|x, {|y, z|}|}" |
|
55 |
"{|x, y|}" == "MPair x y" |
|
56 |
||
57 |
||
2484 | 58 |
constdefs |
59 |
(*Message Y, paired with a MAC computed with the help of X*) |
|
11189 | 60 |
HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset
|
61 |
"Hash[X] Y == {| Hash{|X,Y|}, Y|}" |
2484 | 62 |
|
63 |
(*Keys useful to decrypt elements of a message set*) |
|
11189 | 64 |
keysFor :: "msg set => key set" |
11192 | 65 |
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
1839 | 66 |
|
67 |
(** Inductive definition of all "parts" of a message. **) |
|
68 |
||
11189 | 69 |
consts parts :: "msg set => msg set" |
1839 | 70 |
inductive "parts H" |
11189 | 71 |
intros |
11192 | 72 |
Inj [intro]: "X \<in> H ==> X \<in> parts H" |
73 |
Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H" |
|
74 |
Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H" |
|
75 |
Body: "Crypt K X \<in> parts H ==> X \<in> parts H" |
|
11189 | 76 |
|
77 |
||
78 |
(*Monotonicity*) |
|
79 |
lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" |
|
80 |
apply auto |
|
81 |
apply (erule parts.induct) |
|
82 |
apply (auto dest: Fst Snd Body) |
|
83 |
done |
|
1839 | 84 |
|
85 |
||
1913 | 86 |
(** Inductive definition of "analz" -- what can be broken down from a set of |
1839 | 87 |
messages, including keys. A form of downward closure. Pairs can |
88 |
be taken apart; messages decrypted with known keys. **) |
|
89 |
||
11189 | 90 |
consts analz :: "msg set => msg set" |
1913 | 91 |
inductive "analz H" |
11189 | 92 |
intros |
11192 | 93 |
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" |
94 |
Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H" |
|
95 |
Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H" |
|
11189 | 96 |
Decrypt [dest]: |
11192 | 97 |
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H" |
1839 | 98 |
|
99 |
||
11189 | 100 |
(*Monotonicity; Lemma 1 of Lowe's paper*) |
101 |
lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" |
|
102 |
apply auto |
|
103 |
apply (erule analz.induct) |
|
104 |
apply (auto dest: Fst Snd) |
|
105 |
done |
|
106 |
||
1913 | 107 |
(** Inductive definition of "synth" -- what can be built up from a set of |
1839 | 108 |
messages. A form of upward closure. Pairs can be built, messages |
3668 | 109 |
encrypted with known keys. Agent names are public domain. |
110 |
Numbers can be guessed, but Nonces cannot be. **) |
|
1839 | 111 |
|
11189 | 112 |
consts synth :: "msg set => msg set" |
1913 | 113 |
inductive "synth H" |
11189 | 114 |
intros |
11192 | 115 |
Inj [intro]: "X \<in> H ==> X \<in> synth H" |
116 |
Agent [intro]: "Agent agt \<in> synth H" |
|
117 |
Number [intro]: "Number n \<in> synth H" |
|
118 |
Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H" |
|
119 |
MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H" |
|
120 |
Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H" |
|
11189 | 121 |
|
122 |
(*Monotonicity*) |
|
123 |
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" |
|
124 |
apply auto |
|
125 |
apply (erule synth.induct) |
|
126 |
apply (auto dest: Fst Snd Body) |
|
127 |
done |
|
128 |
||
129 |
(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) |
|
11192 | 130 |
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H" |
131 |
inductive_cases Key_synth [elim!]: "Key K \<in> synth H" |
|
132 |
inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H" |
|
133 |
inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H" |
|
134 |
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H" |
|
11189 | 135 |
|
136 |
use "Message_lemmas.ML" |
|
137 |
||
11251 | 138 |
lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] |
139 |
||
11245 | 140 |
lemma Fake_parts_insert_in_Un: |
141 |
"[|Z \<in> parts (insert X H); X: synth (analz H)|] |
|
142 |
==> Z \<in> synth (analz H) \<union> parts H"; |
|
143 |
by (blast dest: Fake_parts_insert [THEN subsetD, dest]) |
|
144 |
||
11189 | 145 |
method_setup spy_analz = {* |
146 |
Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} |
|
147 |
"for proving the Fake case when analz is involved" |
|
1839 | 148 |
|
11264 | 149 |
method_setup atomic_spy_analz = {* |
150 |
Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *} |
|
151 |
"for debugging spy_analz" |
|
152 |
||
153 |
method_setup Fake_insert_simp = {* |
|
154 |
Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *} |
|
155 |
"for debugging spy_analz" |
|
156 |
||
1839 | 157 |
end |