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 |
Datatype of events;
|
|
7 |
inductive relation "traces" for Needham-Schroeder (shared keys)
|
|
8 |
|
1852
|
9 |
INTERLEAVING? See defn of "traces"
|
|
10 |
|
1839
|
11 |
WHAT ABOUT ASYMMETRIC KEYS? NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
|
|
12 |
PUBLIC KEY...
|
|
13 |
*)
|
|
14 |
|
|
15 |
Event = Message + List +
|
|
16 |
|
|
17 |
consts
|
|
18 |
publicKey :: agent => key
|
1852
|
19 |
serverKey :: agent => key (*symmetric keys*)
|
1839
|
20 |
|
|
21 |
rules
|
|
22 |
isSym_serverKey "isSymKey (serverKey A)"
|
|
23 |
|
1852
|
24 |
consts (*Initial states of agents -- parameter of the construction*)
|
1839
|
25 |
initState :: agent => msg set
|
|
26 |
|
|
27 |
primrec initState agent
|
1852
|
28 |
(*Server knows all keys; other agents know only their own*)
|
1885
|
29 |
initState_Server "initState Server = Key `` range serverKey"
|
1839
|
30 |
initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}"
|
|
31 |
initState_Enemy "initState Enemy = {Key (serverKey Enemy)}"
|
|
32 |
|
|
33 |
(**
|
|
34 |
For asymmetric keys: server knows all public and private keys,
|
|
35 |
others know their private key and perhaps all public keys
|
|
36 |
**)
|
|
37 |
|
|
38 |
datatype (*Messages, and components of agent stores*)
|
|
39 |
event = Says agent agent msg
|
|
40 |
| Notes agent msg
|
|
41 |
|
|
42 |
consts
|
|
43 |
sees1 :: [agent, event] => msg set
|
|
44 |
|
|
45 |
primrec sees1 event
|
|
46 |
(*First agent recalls all that it says, but NOT everything
|
|
47 |
that is sent to it; it must note such things if/when received*)
|
|
48 |
sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})"
|
|
49 |
(*part of A's internal state*)
|
|
50 |
sees1_Notes "sees1 A (Notes A' X) = (if A=A' then {X} else {})"
|
|
51 |
|
|
52 |
consts
|
|
53 |
sees :: [agent, event list] => msg set
|
|
54 |
|
|
55 |
primrec sees list
|
1852
|
56 |
(*Initial knowledge includes all public keys and own private key*)
|
1839
|
57 |
sees_Nil "sees A [] = initState A"
|
|
58 |
sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
|
|
59 |
|
|
60 |
|
|
61 |
constdefs
|
|
62 |
knownBy :: [event list, msg] => agent set
|
|
63 |
"knownBy evs X == {A. X: analyze (sees A evs)}"
|
|
64 |
|
|
65 |
|
1852
|
66 |
(*Agents generate "random" nonces. Different traces always yield
|
|
67 |
different nonces. Same applies for keys.*)
|
|
68 |
(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
|
1839
|
69 |
NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
|
|
70 |
consts
|
1852
|
71 |
newN :: "event list => nat"
|
|
72 |
newK :: "event list => key"
|
1839
|
73 |
|
|
74 |
rules
|
|
75 |
inj_serverKey "inj serverKey"
|
|
76 |
|
|
77 |
inj_newN "inj(newN)"
|
1852
|
78 |
fresh_newN "Nonce (newN evs) ~: parts (initState B)"
|
1839
|
79 |
|
|
80 |
inj_newK "inj(newK)"
|
1852
|
81 |
fresh_newK "Key (newK evs) ~: parts (initState B)"
|
|
82 |
isSym_newK "isSymKey (newK evs)"
|
|
83 |
|
1839
|
84 |
|
1852
|
85 |
(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
|
|
86 |
MOST RECENT message. Does this mean we can't model middleperson attacks?
|
|
87 |
We don't need the most recent restriction in order to handle interception
|
|
88 |
by the Enemy, as agents are not forced to respond anyway.*)
|
1839
|
89 |
|
|
90 |
consts traces :: "event list set"
|
|
91 |
inductive traces
|
|
92 |
intrs
|
|
93 |
Nil "[]: traces"
|
|
94 |
|
|
95 |
(*The enemy MAY say anything he CAN say. We do not expect him to
|
|
96 |
invent new nonces here, but he can also use NS1.*)
|
1852
|
97 |
Fake "[| evs: traces; B ~= Enemy;
|
|
98 |
X: synthesize(analyze(sees Enemy evs))
|
1839
|
99 |
|] ==> (Says Enemy B X) # evs : traces"
|
|
100 |
|
|
101 |
NS1 "[| evs: traces; A ~= Server
|
1852
|
102 |
|] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|})
|
1839
|
103 |
# evs : traces"
|
|
104 |
|
1893
|
105 |
(*We can't trust the sender field, hence the A' in it *)
|
|
106 |
NS2 "[| evs: traces; A ~= B; A ~= Server;
|
|
107 |
evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs'
|
1839
|
108 |
|] ==> (Says Server A
|
1852
|
109 |
(Crypt {|Nonce NA, Agent B, Key (newK evs),
|
|
110 |
(Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
|
|
111 |
(serverKey A))) # evs : traces"
|
|
112 |
|
|
113 |
(*We can't assume S=Server. Agent A "remembers" her nonce.
|
1885
|
114 |
May assume WLOG that she is NOT the Enemy: the Fake rule
|
1852
|
115 |
covers this case. Can inductively show A ~= Server*)
|
|
116 |
NS3 "[| evs: traces; A ~= B;
|
|
117 |
evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
|
|
118 |
(serverKey A)))
|
|
119 |
# evs';
|
|
120 |
A = Friend i;
|
|
121 |
(Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
|
|
122 |
|] ==> (Says A B X) # evs : traces"
|
|
123 |
|
|
124 |
(*Initial version of NS2 had
|
|
125 |
|
|
126 |
{|Agent A, Agent B, Key (newK evs), Nonce NA|}
|
|
127 |
|
|
128 |
for the encrypted part; the version above is LESS transparent, hence
|
|
129 |
maybe HARDER to prove. Also it is precisely as in the BAN paper.
|
|
130 |
*)
|
|
131 |
|
1839
|
132 |
end
|