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
|
1943
|
14 |
shrK :: agent => key (*symmetric keys*)
|
1967
|
15 |
|
1934
|
16 |
rules
|
1943
|
17 |
isSym_shrK "isSymKey (shrK A)"
|
1934
|
18 |
|
|
19 |
consts (*Initial states of agents -- parameter of the construction*)
|
2032
|
20 |
initState :: [agent set, agent] => msg set
|
1934
|
21 |
|
|
22 |
primrec initState agent
|
|
23 |
(*Server knows all keys; other agents know only their own*)
|
2032
|
24 |
initState_Server "initState lost Server = Key `` range shrK"
|
|
25 |
initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}"
|
2064
|
26 |
initState_Spy "initState lost Spy = Key``shrK``lost"
|
2032
|
27 |
|
1934
|
28 |
|
|
29 |
datatype (*Messages, and components of agent stores*)
|
|
30 |
event = Says agent agent msg
|
|
31 |
|
|
32 |
consts
|
|
33 |
sees1 :: [agent, event] => msg set
|
|
34 |
|
|
35 |
primrec sees1 event
|
2078
|
36 |
(*Spy reads all traffic whether addressed to him or not*)
|
|
37 |
sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})"
|
1934
|
38 |
|
|
39 |
consts
|
2032
|
40 |
sees :: [agent set, agent, event list] => msg set
|
1934
|
41 |
|
|
42 |
primrec sees list
|
|
43 |
(*Initial knowledge includes all public keys and own private key*)
|
2032
|
44 |
sees_Nil "sees lost A [] = initState lost A"
|
|
45 |
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
|
1934
|
46 |
|
|
47 |
|
|
48 |
(*Agents generate "random" nonces. Different traces always yield
|
|
49 |
different nonces. Same applies for keys.*)
|
|
50 |
consts
|
|
51 |
newN :: "event list => nat"
|
|
52 |
newK :: "event list => key"
|
|
53 |
|
|
54 |
rules
|
2032
|
55 |
inj_shrK "inj shrK"
|
|
56 |
|
|
57 |
inj_newN "inj newN"
|
1934
|
58 |
|
2032
|
59 |
inj_newK "inj newK"
|
|
60 |
newK_neq_shrK "newK evs ~= shrK A"
|
|
61 |
isSym_newK "isSymKey (newK evs)"
|
1934
|
62 |
|
|
63 |
end
|