author | paulson |
Thu, 19 Dec 1996 11:58:39 +0100 | |
changeset 2451 | ce85a2aafc7a |
parent 2318 | 6d3f7c7f70b0 |
child 2497 | 47de509bdd55 |
permissions | -rw-r--r-- |
2318 | 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 |
||
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
53 |
(*Agents generate "random" nonces, uniquely determined by their argument.*) |
2318 | 54 |
consts |
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
55 |
newN :: nat => nat |
2318 | 56 |
|
57 |
rules |
|
58 |
||
59 |
(*Public keys are disjoint, and never clash with private keys*) |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
60 |
inj_pubK "inj pubK" |
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
61 |
priK_neq_pubK "priK A ~= pubK B" |
2318 | 62 |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset
|
63 |
inj_newN "inj newN" |
2318 | 64 |
|
65 |
end |