1934
|
1 |
(* Title: HOL/Auth/Shared
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1996 University of Cambridge
|
|
5 |
|
|
6 |
Theory of Shared Keys (common to all symmetric-key protocols)
|
|
7 |
|
|
8 |
Server keys; initial states of agents; new nonces and keys; function "sees"
|
|
9 |
*)
|
|
10 |
|
|
11 |
Shared = Message + List +
|
|
12 |
|
|
13 |
consts
|
|
14 |
serverKey :: agent => key (*symmetric keys*)
|
|
15 |
|
|
16 |
rules
|
|
17 |
isSym_serverKey "isSymKey (serverKey A)"
|
|
18 |
|
|
19 |
consts (*Initial states of agents -- parameter of the construction*)
|
|
20 |
initState :: agent => msg set
|
|
21 |
|
|
22 |
primrec initState agent
|
|
23 |
(*Server knows all keys; other agents know only their own*)
|
|
24 |
initState_Server "initState Server = Key `` range serverKey"
|
|
25 |
initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}"
|
|
26 |
initState_Enemy "initState Enemy = {Key (serverKey Enemy)}"
|
|
27 |
|
|
28 |
datatype (*Messages, and components of agent stores*)
|
|
29 |
event = Says agent agent msg
|
|
30 |
| Notes agent msg
|
|
31 |
|
|
32 |
consts
|
|
33 |
sees1 :: [agent, event] => msg set
|
|
34 |
|
|
35 |
primrec sees1 event
|
|
36 |
(*First agent recalls all that it says, but NOT everything
|
|
37 |
that is sent to it; it must note such things if/when received*)
|
|
38 |
sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})"
|
|
39 |
(*part of A's internal state*)
|
|
40 |
sees1_Notes "sees1 A (Notes A' X) = (if A=A' then {X} else {})"
|
|
41 |
|
|
42 |
consts
|
|
43 |
sees :: [agent, event list] => msg set
|
|
44 |
|
|
45 |
primrec sees list
|
|
46 |
(*Initial knowledge includes all public keys and own private key*)
|
|
47 |
sees_Nil "sees A [] = initState A"
|
|
48 |
sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
|
|
49 |
|
|
50 |
|
|
51 |
(*Agents generate "random" nonces. Different traces always yield
|
|
52 |
different nonces. Same applies for keys.*)
|
|
53 |
consts
|
|
54 |
newN :: "event list => nat"
|
|
55 |
newK :: "event list => key"
|
|
56 |
|
|
57 |
rules
|
|
58 |
inj_serverKey "inj serverKey"
|
|
59 |
|
|
60 |
inj_newN "inj newN"
|
|
61 |
fresh_newN "Nonce (newN evs) ~: parts (initState B)"
|
|
62 |
|
|
63 |
inj_newK "inj newK"
|
|
64 |
fresh_newK "Key (newK evs) ~: parts (initState B)"
|
|
65 |
isSym_newK "isSymKey (newK evs)"
|
|
66 |
|
|
67 |
end
|