author | paulson |
Thu, 26 Sep 1996 12:50:48 +0200 | |
changeset 2032 | 1bbf1bdcaf56 |
parent 1942 | 6c9c1a42a869 |
permissions | -rw-r--r-- |
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 |
|
1942 | 19 |
shrK :: agent => key (*symmetric keys*) |
1839 | 20 |
|
21 |
rules |
|
1942 | 22 |
isSym_shrK "isSymKey (shrK A)" |
1839 | 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*) |
1942 | 29 |
initState_Server "initState Server = Key `` range shrK" |
30 |
initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" |
|
2032 | 31 |
initState_Spy "initState Spy = {Key (shrK Spy)}" |
1839 | 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*) |
|
2032 | 48 |
sees1_Says "sees1 A (Says A' B X) = (if A:{A',Spy} then {X} else {})" |
1839 | 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 |
|
1913 | 63 |
"knownBy evs X == {A. X: analz (sees A evs)}" |
1839 | 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 |
|
1942 | 75 |
inj_shrK "inj shrK" |
1839 | 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 |
|
1930 | 85 |
(*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*) |
1839 | 86 |
consts traces :: "event list set" |
87 |
inductive traces |
|
88 |
intrs |
|
1930 | 89 |
(*Initial trace is empty*) |
1839 | 90 |
Nil "[]: traces" |
91 |
||
2032 | 92 |
(*The spy MAY say anything he CAN say. We do not expect him to |
1930 | 93 |
invent new nonces here, but he can also use NS1. Common to |
94 |
all similar protocols.*) |
|
2032 | 95 |
Fake "[| evs: traces; B ~= Spy; X: synth (analz (sees Spy evs)) |
96 |
|] ==> (Says Spy B X) # evs : traces" |
|
1839 | 97 |
|
1930 | 98 |
(*Alice initiates a protocol run*) |
1839 | 99 |
NS1 "[| evs: traces; A ~= Server |
1852 | 100 |
|] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) |
1839 | 101 |
# evs : traces" |
102 |
||
1930 | 103 |
(*Server's response to Alice's message. |
104 |
!! It may respond more than once to A's request !! |
|
1933 | 105 |
Server doesn't know who the true sender is, hence the A' in |
106 |
the sender field.*) |
|
1893 | 107 |
NS2 "[| evs: traces; A ~= B; A ~= Server; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
108 |
(Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs |
1839 | 109 |
|] ==> (Says Server A |
1852 | 110 |
(Crypt {|Nonce NA, Agent B, Key (newK evs), |
1942 | 111 |
(Crypt {|Key (newK evs), Agent A|} (shrK B))|} |
112 |
(shrK A))) # evs : traces" |
|
1852 | 113 |
|
1930 | 114 |
(*We can't assume S=Server. Agent A "remembers" her nonce. |
2032 | 115 |
May assume WLOG that she is NOT the Spy: the Fake rule |
1930 | 116 |
covers this case. Can inductively show A ~= Server*) |
1852 | 117 |
NS3 "[| evs: traces; A ~= B; |
1942 | 118 |
(Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
119 |
: set_of_list evs; |
1852 | 120 |
A = Friend i; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
121 |
(Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs |
1852 | 122 |
|] ==> (Says A B X) # evs : traces" |
123 |
||
1933 | 124 |
(*Bob's nonce exchange. He does not know who the message came |
125 |
from, but responds to A because she is mentioned inside.*) |
|
1930 | 126 |
NS4 "[| evs: traces; A ~= B; |
1942 | 127 |
(Says A' B (Crypt {|Key K, Agent A|} (shrK B))) |
1930 | 128 |
: set_of_list evs |
129 |
|] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces" |
|
1933 | 130 |
|
131 |
(*Alice responds with (Suc N), if she has seen the key before.*) |
|
132 |
NS5 "[| evs: traces; A ~= B; |
|
133 |
(Says B' A (Crypt (Nonce N) K)) : set_of_list evs; |
|
1942 | 134 |
(Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) |
1933 | 135 |
: set_of_list evs |
136 |
|] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces" |
|
137 |
||
1839 | 138 |
end |