author | berghofe |
Fri, 24 Jul 1998 13:03:20 +0200 | |
changeset 5183 | 89f162de39cf |
parent 3683 | aafe719dff14 |
child 6308 | 76f3865a2b1d |
permissions | -rw-r--r-- |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Auth/Event |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
4 |
Copyright 1996 University of Cambridge |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
5 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
6 |
Theory of events for security protocols |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
7 |
|
3683 | 8 |
Datatype of events; function "spies"; freshness |
3678 | 9 |
|
3683 | 10 |
"bad" agents have been broken by the Spy; their private keys and internal |
3678 | 11 |
stores are visible to him |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
12 |
*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
13 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
14 |
Event = Message + List + |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
15 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
16 |
consts (*Initial states of agents -- parameter of the construction*) |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
17 |
initState :: agent => msg set |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
18 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
19 |
datatype (*Messages--could add another constructor for agent knowledge*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
20 |
event = Says agent agent msg |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
21 |
| Notes agent msg |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
22 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
23 |
consts |
3683 | 24 |
bad :: agent set (*compromised agents*) |
25 |
spies :: event list => msg set |
|
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
26 |
|
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
27 |
rules |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
28 |
(*Spy has access to his own key for spoof messages, but Server is secure*) |
3683 | 29 |
Spy_in_bad "Spy: bad" |
30 |
Server_not_bad "Server ~: bad" |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
31 |
|
5183 | 32 |
primrec |
3678 | 33 |
(*Spy reads all traffic whether addressed to him or not*) |
3683 | 34 |
spies_Nil "spies [] = initState Spy" |
35 |
spies_Cons "spies (ev # evs) = |
|
36 |
(case ev of |
|
37 |
Says A B X => insert X (spies evs) |
|
38 |
| Notes A X => |
|
39 |
if A:bad then insert X (spies evs) else spies evs)" |
|
3678 | 40 |
|
3683 | 41 |
consts |
42 |
(*Set of items that might be visible to somebody: |
|
43 |
complement of the set of fresh items*) |
|
44 |
used :: event list => msg set |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
45 |
|
5183 | 46 |
primrec |
3683 | 47 |
used_Nil "used [] = (UN B. parts (initState B))" |
48 |
used_Cons "used (ev # evs) = |
|
49 |
(case ev of |
|
50 |
Says A B X => parts {X} Un (used evs) |
|
51 |
| Notes A X => parts {X} Un (used evs))" |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
52 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
53 |
end |