author | paulson |
Mon, 14 Jul 1997 12:47:21 +0200 | |
changeset 3519 | ab0a9fbed4c0 |
parent 3512 | 9dcb4daa15e8 |
child 3678 | 414e04d7c2d6 |
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 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
8 |
Datatype of events; function "sees"; freshness |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
9 |
*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
10 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
11 |
Event = Message + List + |
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 |
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
|
14 |
initState :: agent => msg set |
3512
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 |
datatype (*Messages--could add another constructor for agent knowledge*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
17 |
event = Says agent agent msg |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
18 |
| Notes agent msg |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
19 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
20 |
consts |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
21 |
sees1 :: [agent, event] => msg set |
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 |
primrec sees1 event |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
24 |
(*Spy reads all traffic whether addressed to him or not*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
25 |
sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
26 |
sees1_Notes "sees1 A (Notes A' X) = (if A = A' then {X} else {})" |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
27 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
28 |
consts |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
29 |
lost :: agent set (*agents whose private keys have been compromised*) |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
30 |
sees :: [agent, event list] => msg set |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
31 |
|
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
32 |
rules |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
33 |
(*Spy has access to his own key for spoof messages, but Server is secure*) |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
34 |
Spy_in_lost "Spy: lost" |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
35 |
Server_not_lost "Server ~: lost" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
36 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
37 |
primrec sees list |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
38 |
sees_Nil "sees A [] = initState A" |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
39 |
sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
40 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
41 |
constdefs |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
42 |
(*Set of items that might be visible to somebody: complement of the set |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
43 |
of fresh items*) |
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
44 |
used :: event list => msg set |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
45 |
"used evs == parts (UN B. sees B evs)" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
46 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
47 |
end |