|
1 (* Title: HOL/Auth/Public |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Theory of Public Keys (common to all symmetric-key protocols) |
|
7 |
|
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
|
9 *) |
|
10 |
|
11 Public = Message + List + |
|
12 |
|
13 consts |
|
14 pubK :: agent => key |
|
15 |
|
16 syntax |
|
17 priK :: agent => key |
|
18 |
|
19 translations |
|
20 "priK x" == "invKey(pubK x)" |
|
21 |
|
22 consts (*Initial states of agents -- parameter of the construction*) |
|
23 initState :: [agent set, agent] => msg set |
|
24 |
|
25 primrec initState agent |
|
26 (*Agents know their private key and all public keys*) |
|
27 initState_Server "initState lost Server = |
|
28 insert (Key (priK Server)) (Key `` range pubK)" |
|
29 initState_Friend "initState lost (Friend i) = |
|
30 insert (Key (priK (Friend i))) (Key `` range pubK)" |
|
31 initState_Spy "initState lost Spy = |
|
32 (Key``invKey``pubK``lost) Un (Key `` range pubK)" |
|
33 |
|
34 |
|
35 datatype (*Messages, and components of agent stores*) |
|
36 event = Says agent agent msg |
|
37 |
|
38 consts |
|
39 sees1 :: [agent, event] => msg set |
|
40 |
|
41 primrec sees1 event |
|
42 (*Spy reads all traffic whether addressed to him or not*) |
|
43 sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" |
|
44 |
|
45 consts |
|
46 sees :: [agent set, agent, event list] => msg set |
|
47 |
|
48 primrec sees list |
|
49 sees_Nil "sees lost A [] = initState lost A" |
|
50 sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" |
|
51 |
|
52 |
|
53 (*Agents generate "random" nonces. These are uniquely determined by |
|
54 the length of their argument, a trace.*) |
|
55 consts |
|
56 newN :: "event list => nat" |
|
57 |
|
58 rules |
|
59 |
|
60 (*Public keys are disjoint, and never clash with private keys*) |
|
61 inj_pubK "inj pubK" |
|
62 priK_neq_pubK "priK A ~= pubK B" |
|
63 |
|
64 newN_length "(newN evs = newN evt) ==> (length evs = length evt)" |
|
65 |
|
66 end |