paulson@1839
|
1 |
(* Title: HOL/Auth/Message
|
paulson@1839
|
2 |
ID: $Id$
|
paulson@1839
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@1839
|
4 |
Copyright 1996 University of Cambridge
|
paulson@1839
|
5 |
|
paulson@1839
|
6 |
Datatypes of agents and messages;
|
paulson@1913
|
7 |
Inductive relations "parts", "analz" and "synth"
|
paulson@1839
|
8 |
*)
|
paulson@1839
|
9 |
|
paulson@1839
|
10 |
Message = Arith +
|
paulson@1839
|
11 |
|
paulson@1839
|
12 |
(*Is there a difference between a nonce and arbitrary numerical data?
|
paulson@1839
|
13 |
Do we need a type of nonces?*)
|
paulson@1839
|
14 |
|
paulson@1839
|
15 |
types
|
paulson@1839
|
16 |
key = nat
|
paulson@1839
|
17 |
|
paulson@1839
|
18 |
consts
|
paulson@1839
|
19 |
invKey :: key=>key
|
paulson@1839
|
20 |
|
paulson@1839
|
21 |
rules
|
paulson@1839
|
22 |
invKey "invKey (invKey K) = K"
|
paulson@1839
|
23 |
|
paulson@1839
|
24 |
(*The inverse of a symmetric key is itself;
|
paulson@1839
|
25 |
that of a public key is the private key and vice versa*)
|
paulson@1839
|
26 |
|
paulson@1839
|
27 |
constdefs
|
paulson@1839
|
28 |
isSymKey :: key=>bool
|
paulson@1839
|
29 |
"isSymKey K == (invKey K = K)"
|
paulson@1839
|
30 |
|
paulson@1839
|
31 |
datatype (*We allow any number of friendly agents*)
|
paulson@2032
|
32 |
agent = Server | Friend nat | Spy
|
paulson@1839
|
33 |
|
paulson@1839
|
34 |
datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)
|
paulson@1839
|
35 |
msg = Agent agent
|
paulson@1839
|
36 |
| Nonce nat
|
paulson@1839
|
37 |
| Key key
|
paulson@2373
|
38 |
| Hash msg
|
paulson@1839
|
39 |
| MPair msg msg
|
paulson@2284
|
40 |
| Crypt key msg
|
paulson@1839
|
41 |
|
paulson@1839
|
42 |
(*Allows messages of the form {|A,B,NA|}, etc...*)
|
paulson@1839
|
43 |
syntax
|
paulson@2516
|
44 |
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
|
paulson@1839
|
45 |
|
paulson@1839
|
46 |
translations
|
paulson@1839
|
47 |
"{|x, y, z|}" == "{|x, {|y, z|}|}"
|
paulson@1839
|
48 |
"{|x, y|}" == "MPair x y"
|
paulson@1839
|
49 |
|
paulson@1839
|
50 |
|
paulson@2484
|
51 |
constdefs
|
paulson@2484
|
52 |
(*Message Y, paired with a MAC computed with the help of X*)
|
paulson@2516
|
53 |
HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000])
|
paulson@2516
|
54 |
"Hash[X] Y == {| Hash{|X,Y|}, Y|}"
|
paulson@2484
|
55 |
|
paulson@2484
|
56 |
(*Keys useful to decrypt elements of a message set*)
|
paulson@1839
|
57 |
keysFor :: msg set => key set
|
paulson@2284
|
58 |
"keysFor H == invKey `` {K. EX X. Crypt K X : H}"
|
paulson@1839
|
59 |
|
paulson@1839
|
60 |
(** Inductive definition of all "parts" of a message. **)
|
paulson@1839
|
61 |
|
paulson@1839
|
62 |
consts parts :: msg set => msg set
|
paulson@1839
|
63 |
inductive "parts H"
|
paulson@1839
|
64 |
intrs
|
paulson@2373
|
65 |
Inj "X: H ==> X: parts H"
|
paulson@2373
|
66 |
Fst "{|X,Y|} : parts H ==> X : parts H"
|
paulson@2373
|
67 |
Snd "{|X,Y|} : parts H ==> Y : parts H"
|
paulson@2284
|
68 |
Body "Crypt K X : parts H ==> X : parts H"
|
paulson@1839
|
69 |
|
paulson@1839
|
70 |
|
paulson@1913
|
71 |
(** Inductive definition of "analz" -- what can be broken down from a set of
|
paulson@1839
|
72 |
messages, including keys. A form of downward closure. Pairs can
|
paulson@1839
|
73 |
be taken apart; messages decrypted with known keys. **)
|
paulson@1839
|
74 |
|
paulson@1913
|
75 |
consts analz :: msg set => msg set
|
paulson@1913
|
76 |
inductive "analz H"
|
paulson@1839
|
77 |
intrs
|
paulson@1913
|
78 |
Inj "X: H ==> X: analz H"
|
paulson@1913
|
79 |
Fst "{|X,Y|} : analz H ==> X : analz H"
|
paulson@1913
|
80 |
Snd "{|X,Y|} : analz H ==> Y : analz H"
|
paulson@2284
|
81 |
Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
|
paulson@1839
|
82 |
|
paulson@1839
|
83 |
|
paulson@1913
|
84 |
(** Inductive definition of "synth" -- what can be built up from a set of
|
paulson@1839
|
85 |
messages. A form of upward closure. Pairs can be built, messages
|
paulson@1839
|
86 |
encrypted with known keys. Agent names may be quoted. **)
|
paulson@1839
|
87 |
|
paulson@1913
|
88 |
consts synth :: msg set => msg set
|
paulson@1913
|
89 |
inductive "synth H"
|
paulson@1839
|
90 |
intrs
|
paulson@1913
|
91 |
Inj "X: H ==> X: synth H"
|
paulson@1913
|
92 |
Agent "Agent agt : synth H"
|
paulson@2373
|
93 |
Hash "X: synth H ==> Hash X : synth H"
|
paulson@1913
|
94 |
MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H"
|
paulson@2373
|
95 |
Crypt "[| X: synth H; Key(K) : H |] ==> Crypt K X : synth H"
|
paulson@1839
|
96 |
|
paulson@1839
|
97 |
end
|