equal
deleted
inserted
replaced
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Theory of Shared Keys (common to all symmetric-key protocols) |
6 Theory of Shared Keys (common to all symmetric-key protocols) |
7 |
7 |
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
9 |
|
10 IS THE Notes constructor needed?? |
|
11 *) |
9 *) |
12 |
10 |
13 Shared = Message + List + |
11 Shared = Message + List + |
14 |
12 |
15 consts |
13 consts |
31 initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" |
29 initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" |
32 initState_Enemy "initState Enemy = Key``shrK``bad" |
30 initState_Enemy "initState Enemy = Key``shrK``bad" |
33 |
31 |
34 datatype (*Messages, and components of agent stores*) |
32 datatype (*Messages, and components of agent stores*) |
35 event = Says agent agent msg |
33 event = Says agent agent msg |
36 | Notes agent msg |
|
37 |
34 |
38 consts |
35 consts |
39 sees1 :: [agent, event] => msg set |
36 sees1 :: [agent, event] => msg set |
40 |
37 |
41 primrec sees1 event |
38 primrec sees1 event |
42 (*First agent recalls all that it says, but NOT everything |
39 (*First agent recalls all that it says, but NOT everything |
43 that is sent to it; it must note such things if/when received*) |
40 that is sent to it; it must note such things if/when received*) |
44 sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})" |
41 sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})" |
45 (*part of A's internal state*) |
42 (*part of A's internal state*) |
46 sees1_Notes "sees1 A (Notes A' X) = (if A=A' then {X} else {})" |
|
47 |
43 |
48 consts |
44 consts |
49 sees :: [agent, event list] => msg set |
45 sees :: [agent, event list] => msg set |
50 |
46 |
51 primrec sees list |
47 primrec sees list |