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;
|
|
7 |
Inductive relations "parts", "analyze" and "synthesize"
|
|
8 |
*)
|
|
9 |
|
|
10 |
Message = Arith +
|
|
11 |
|
|
12 |
(*Is there a difference between a nonce and arbitrary numerical data?
|
|
13 |
Do we need a type of nonces?*)
|
|
14 |
|
|
15 |
types
|
|
16 |
key = nat
|
|
17 |
|
|
18 |
consts
|
|
19 |
invKey :: key=>key
|
|
20 |
|
|
21 |
rules
|
|
22 |
invKey "invKey (invKey K) = K"
|
|
23 |
|
|
24 |
(*The inverse of a symmetric key is itself;
|
|
25 |
that of a public key is the private key and vice versa*)
|
|
26 |
|
|
27 |
constdefs
|
|
28 |
isSymKey :: key=>bool
|
|
29 |
"isSymKey K == (invKey K = K)"
|
|
30 |
|
|
31 |
(*We do not assume Crypt (Crypt X K) (invKey K) = X
|
|
32 |
because Crypt is a constructor! We assume that encryption is injective,
|
|
33 |
which is not true in the real world. The alternative is to take
|
|
34 |
Crypt as an uninterpreted function symbol satisfying the equation
|
|
35 |
above. This seems to require moving to ZF and regarding msg as an
|
|
36 |
inductive definition instead of a datatype.*)
|
|
37 |
|
|
38 |
datatype (*We allow any number of friendly agents*)
|
|
39 |
agent = Server | Friend nat | Enemy
|
|
40 |
|
|
41 |
consts
|
|
42 |
isEnemy :: agent => bool
|
|
43 |
|
|
44 |
primrec isEnemy agent
|
|
45 |
isEnemy_Server "isEnemy Server = False"
|
|
46 |
isEnemy_Friend "isEnemy (Friend i) = False"
|
|
47 |
isEnemy_Enemy "isEnemy Enemy = True"
|
|
48 |
|
|
49 |
datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)
|
|
50 |
msg = Agent agent
|
|
51 |
| Nonce nat
|
|
52 |
| Key key
|
|
53 |
| MPair msg msg
|
|
54 |
| Crypt msg key
|
|
55 |
|
|
56 |
(*Allows messages of the form {|A,B,NA|}, etc...*)
|
|
57 |
syntax
|
|
58 |
"@MTuple" :: "['a, args] => 'a * 'b" ("(1{|_,/ _|})")
|
|
59 |
|
|
60 |
translations
|
|
61 |
"{|x, y, z|}" == "{|x, {|y, z|}|}"
|
|
62 |
"{|x, y|}" == "MPair x y"
|
|
63 |
|
|
64 |
|
|
65 |
constdefs (*Keys useful to decrypt elements of a message set*)
|
|
66 |
keysFor :: msg set => key set
|
|
67 |
"keysFor H == invKey `` {K. EX X. Crypt X K : H}"
|
|
68 |
|
|
69 |
(** Inductive definition of all "parts" of a message. **)
|
|
70 |
|
|
71 |
consts parts :: msg set => msg set
|
|
72 |
inductive "parts H"
|
|
73 |
intrs
|
|
74 |
Inj "X: H ==> X: parts H"
|
|
75 |
Fst "{|X,Y|} : parts H ==> X : parts H"
|
|
76 |
Snd "{|X,Y|} : parts H ==> Y : parts H"
|
|
77 |
Body "Crypt X K : parts H ==> X : parts H"
|
|
78 |
|
|
79 |
|
|
80 |
(** Inductive definition of "analyze" -- what can be broken down from a set of
|
|
81 |
messages, including keys. A form of downward closure. Pairs can
|
|
82 |
be taken apart; messages decrypted with known keys. **)
|
|
83 |
|
|
84 |
consts analyze :: msg set => msg set
|
|
85 |
inductive "analyze H"
|
|
86 |
intrs
|
|
87 |
Inj "X: H ==> X: analyze H"
|
|
88 |
|
|
89 |
Fst "{|X,Y|} : analyze H ==> X : analyze H"
|
|
90 |
|
|
91 |
Snd "{|X,Y|} : analyze H ==> Y : analyze H"
|
|
92 |
|
|
93 |
Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
|
|
94 |
|] ==> X : analyze H"
|
|
95 |
|
|
96 |
|
|
97 |
(** Inductive definition of "synthesize" -- what can be built up from a set of
|
|
98 |
messages. A form of upward closure. Pairs can be built, messages
|
|
99 |
encrypted with known keys. Agent names may be quoted. **)
|
|
100 |
|
|
101 |
consts synthesize :: msg set => msg set
|
|
102 |
inductive "synthesize H"
|
|
103 |
intrs
|
|
104 |
Inj "X: H ==> X: synthesize H"
|
|
105 |
|
|
106 |
Agent "Agent agt : synthesize H"
|
|
107 |
|
|
108 |
MPair "[| X: synthesize H; Y: synthesize H
|
|
109 |
|] ==> {|X,Y|} : synthesize H"
|
|
110 |
|
|
111 |
Crypt "[| X: synthesize H; Key(K): synthesize H
|
|
112 |
|] ==> Crypt X K : synthesize H"
|
|
113 |
|
|
114 |
end
|