author | paulson |
Tue, 01 Jul 1997 10:39:28 +0200 | |
changeset 3472 | fb3c38c88c08 |
parent 3414 | 804c8a178a7f |
child 3512 | 9dcb4daa15e8 |
permissions | -rw-r--r-- |
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 |
||
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
11 |
Shared = Message + List + Finite + |
1934 | 12 |
|
13 |
consts |
|
1943 | 14 |
shrK :: agent => key (*symmetric keys*) |
1967 | 15 |
|
1934 | 16 |
rules |
3472
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3414
diff
changeset
|
17 |
isSym_keys "isSymKey K" (*All keys are symmetric*) |
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3414
diff
changeset
|
18 |
inj_shrK "inj shrK" (*No two agents have the same long-term key*) |
1934 | 19 |
|
20 |
consts (*Initial states of agents -- parameter of the construction*) |
|
2032 | 21 |
initState :: [agent set, agent] => msg set |
1934 | 22 |
|
23 |
primrec initState agent |
|
2319 | 24 |
(*Server knows all long-term keys; other agents know only their own*) |
2032 | 25 |
initState_Server "initState lost Server = Key `` range shrK" |
26 |
initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}" |
|
2064 | 27 |
initState_Spy "initState lost Spy = Key``shrK``lost" |
2032 | 28 |
|
1934 | 29 |
|
30 |
datatype (*Messages, and components of agent stores*) |
|
31 |
event = Says agent agent msg |
|
32 |
||
33 |
consts |
|
34 |
sees1 :: [agent, event] => msg set |
|
35 |
||
36 |
primrec sees1 event |
|
2078 | 37 |
(*Spy reads all traffic whether addressed to him or not*) |
38 |
sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" |
|
1934 | 39 |
|
40 |
consts |
|
2032 | 41 |
sees :: [agent set, agent, event list] => msg set |
1934 | 42 |
|
43 |
primrec sees list |
|
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 |
||
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
48 |
constdefs |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
49 |
(*Set of items that might be visible to somebody: complement of the set |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
50 |
of fresh items*) |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
51 |
used :: event list => msg set |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
52 |
"used evs == parts (UN lost B. sees lost B evs)" |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
53 |
|
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
54 |
|
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
55 |
rules |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
56 |
(*Unlike the corresponding property of nonces, this cannot be proved. |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
57 |
We have infinitely many agents and there is nothing to stop their |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
58 |
long-term keys from exhausting all the natural numbers. The axiom |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
59 |
assumes that their keys are dispersed so as to leave room for infinitely |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
60 |
many fresh session keys. We could, alternatively, restrict agents to |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
61 |
an unspecified finite number.*) |
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
2516
diff
changeset
|
62 |
Key_supply_ax "finite KK ==> EX K. K ~: KK & Key K ~: used evs" |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
63 |
|
1934 | 64 |
end |