|
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 |