equal
deleted
inserted
replaced
35 above. This seems to require moving to ZF and regarding msg as an |
35 above. This seems to require moving to ZF and regarding msg as an |
36 inductive definition instead of a datatype.*) |
36 inductive definition instead of a datatype.*) |
37 |
37 |
38 datatype (*We allow any number of friendly agents*) |
38 datatype (*We allow any number of friendly agents*) |
39 agent = Server | Friend nat | Spy |
39 agent = Server | Friend nat | Spy |
40 |
|
41 consts |
|
42 isSpy :: agent => bool |
|
43 |
|
44 primrec isSpy agent |
|
45 isSpy_Server "isSpy Server = False" |
|
46 isSpy_Friend "isSpy (Friend i) = False" |
|
47 isSpy_Spy "isSpy Spy = True" |
|
48 |
40 |
49 datatype (*Messages are agent names, nonces, keys, pairs and encryptions*) |
41 datatype (*Messages are agent names, nonces, keys, pairs and encryptions*) |
50 msg = Agent agent |
42 msg = Agent agent |
51 | Nonce nat |
43 | Nonce nat |
52 | Key key |
44 | Key key |