|
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 Datatype of events; |
|
7 inductive relation "traces" for Needham-Schroeder (shared keys) |
|
8 |
|
9 WHAT ABOUT ASYMMETRIC KEYS? NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S |
|
10 PUBLIC KEY... |
|
11 *) |
|
12 |
|
13 Event = Message + List + |
|
14 |
|
15 consts |
|
16 publicKey :: agent => key |
|
17 serverKey :: agent => key (*symmetric keys*) |
|
18 |
|
19 rules |
|
20 isSym_serverKey "isSymKey (serverKey A)" |
|
21 |
|
22 consts (*Initial states of agents -- parameter of the construction*) |
|
23 initState :: agent => msg set |
|
24 |
|
25 primrec initState agent |
|
26 (*Server knows all keys; other agents know only their own*) |
|
27 initState_Server "initState Server = range (Key o serverKey)" |
|
28 initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}" |
|
29 initState_Enemy "initState Enemy = {Key (serverKey Enemy)}" |
|
30 |
|
31 (** |
|
32 For asymmetric keys: server knows all public and private keys, |
|
33 others know their private key and perhaps all public keys |
|
34 **) |
|
35 |
|
36 datatype (*Messages, and components of agent stores*) |
|
37 event = Says agent agent msg |
|
38 | Notes agent msg |
|
39 |
|
40 consts |
|
41 sees1 :: [agent, event] => msg set |
|
42 |
|
43 primrec sees1 event |
|
44 (*First agent recalls all that it says, but NOT everything |
|
45 that is sent to it; it must note such things if/when received*) |
|
46 sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})" |
|
47 (*part of A's internal state*) |
|
48 sees1_Notes "sees1 A (Notes A' X) = (if A=A' then {X} else {})" |
|
49 |
|
50 consts |
|
51 sees :: [agent, event list] => msg set |
|
52 |
|
53 primrec sees list |
|
54 (*Initial knowledge includes all public keys and own private key*) |
|
55 sees_Nil "sees A [] = initState A" |
|
56 sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs" |
|
57 |
|
58 |
|
59 constdefs |
|
60 knownBy :: [event list, msg] => agent set |
|
61 "knownBy evs X == {A. X: analyze (sees A evs)}" |
|
62 |
|
63 |
|
64 (*Agents generate "random" nonces. Different agents always generate |
|
65 different nonces. Different traces also yield different nonces. Same |
|
66 applies for keys.*) |
|
67 (*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS. REMOVE AGENT ARGUMENT? |
|
68 NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*) |
|
69 consts |
|
70 newN :: "agent * event list => nat" |
|
71 newK :: "agent * event list => key" |
|
72 |
|
73 rules |
|
74 inj_serverKey "inj serverKey" |
|
75 |
|
76 inj_newN "inj(newN)" |
|
77 fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" |
|
78 |
|
79 inj_newK "inj(newK)" |
|
80 fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" |
|
81 isSym_newK "isSymKey (newK(A,evs))" |
|
82 |
|
83 |
|
84 consts traces :: "event list set" |
|
85 inductive traces |
|
86 intrs |
|
87 Nil "[]: traces" |
|
88 |
|
89 (*The enemy MAY say anything he CAN say. We do not expect him to |
|
90 invent new nonces here, but he can also use NS1.*) |
|
91 Fake "[| evs: traces; X: synthesize(analyze(sees Enemy evs)) |
|
92 |] ==> (Says Enemy B X) # evs : traces" |
|
93 |
|
94 NS1 "[| evs: traces; A ~= Server |
|
95 |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) |
|
96 # evs : traces" |
|
97 |
|
98 NS2 "[| evs: traces; |
|
99 evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs' |
|
100 |] ==> (Says Server A |
|
101 (Crypt {|Agent A, Agent B, |
|
102 Key (newK(Server,evs)), Nonce NA|} |
|
103 (serverKey A))) # evs : traces" |
|
104 end |