11250
|
1 |
(* Title: HOL/Auth/Event
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1996 University of Cambridge
|
|
5 |
|
|
6 |
Theory of events for security protocols
|
|
7 |
|
|
8 |
Datatype of events; function "spies"; freshness
|
|
9 |
|
|
10 |
"bad" agents have been broken by the Spy; their private keys and internal
|
|
11 |
stores are visible to him
|
|
12 |
*)
|
|
13 |
|
16417
|
14 |
theory Event imports Message
|
|
15 |
uses ("Event_lemmas.ML") begin
|
11250
|
16 |
|
|
17 |
consts (*Initial states of agents -- parameter of the construction*)
|
|
18 |
initState :: "agent => msg set"
|
|
19 |
|
|
20 |
datatype
|
|
21 |
event = Says agent agent msg
|
|
22 |
| Gets agent msg
|
|
23 |
| Notes agent msg
|
|
24 |
|
|
25 |
consts
|
|
26 |
bad :: "agent set" (*compromised agents*)
|
|
27 |
knows :: "agent => event list => msg set"
|
|
28 |
|
|
29 |
|
11310
|
30 |
(*"spies" is retained for compatibility's sake*)
|
11250
|
31 |
syntax
|
|
32 |
spies :: "event list => msg set"
|
|
33 |
|
|
34 |
translations
|
|
35 |
"spies" => "knows Spy"
|
|
36 |
|
|
37 |
|
|
38 |
axioms
|
|
39 |
(*Spy has access to his own key for spoof messages, but Server is secure*)
|
|
40 |
Spy_in_bad [iff] : "Spy \<in> bad"
|
|
41 |
Server_not_bad [iff] : "Server \<notin> bad"
|
|
42 |
|
|
43 |
primrec
|
|
44 |
knows_Nil: "knows A [] = initState A"
|
|
45 |
knows_Cons:
|
|
46 |
"knows A (ev # evs) =
|
|
47 |
(if A = Spy then
|
|
48 |
(case ev of
|
|
49 |
Says A' B X => insert X (knows Spy evs)
|
|
50 |
| Gets A' X => knows Spy evs
|
|
51 |
| Notes A' X =>
|
|
52 |
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
|
|
53 |
else
|
|
54 |
(case ev of
|
|
55 |
Says A' B X =>
|
|
56 |
if A'=A then insert X (knows A evs) else knows A evs
|
|
57 |
| Gets A' X =>
|
|
58 |
if A'=A then insert X (knows A evs) else knows A evs
|
|
59 |
| Notes A' X =>
|
|
60 |
if A'=A then insert X (knows A evs) else knows A evs))"
|
|
61 |
|
|
62 |
(*
|
|
63 |
Case A=Spy on the Gets event
|
|
64 |
enforces the fact that if a message is received then it must have been sent,
|
|
65 |
therefore the oops case must use Notes
|
|
66 |
*)
|
|
67 |
|
|
68 |
consts
|
|
69 |
(*Set of items that might be visible to somebody:
|
|
70 |
complement of the set of fresh items*)
|
|
71 |
used :: "event list => msg set"
|
|
72 |
|
|
73 |
primrec
|
|
74 |
used_Nil: "used [] = (UN B. parts (initState B))"
|
|
75 |
used_Cons: "used (ev # evs) =
|
|
76 |
(case ev of
|
|
77 |
Says A B X => parts {X} Un (used evs)
|
|
78 |
| Gets A X => used evs
|
|
79 |
| Notes A X => parts {X} Un (used evs))"
|
|
80 |
|
|
81 |
|
|
82 |
use "Event_lemmas.ML"
|
|
83 |
|
|
84 |
method_setup analz_mono_contra = {*
|
|
85 |
Method.no_args
|
|
86 |
(Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
|
|
87 |
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
|
|
88 |
|
|
89 |
end
|