author | paulson |
Sat, 19 May 2001 12:19:23 +0200 | |
changeset 11310 | 51e70b7bc315 |
parent 11192 | 5fd02b905a9a |
child 11463 | 96b5b27da55c |
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 |
|
11104 | 14 |
theory Event = Message |
15 |
files ("Event_lemmas.ML"): |
|
16 |
||
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
17 |
consts (*Initial states of agents -- parameter of the construction*) |
11104 | 18 |
initState :: "agent => msg set" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
19 |
|
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
20 |
datatype |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
21 |
event = Says agent agent msg |
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
22 |
| Gets agent msg |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
23 |
| Notes agent msg |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
24 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
25 |
consts |
11104 | 26 |
bad :: "agent set" (*compromised agents*) |
27 |
knows :: "agent => event list => msg set" |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
28 |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
29 |
|
11310 | 30 |
(*"spies" is retained for compatibility's sake*) |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
31 |
syntax |
11104 | 32 |
spies :: "event list => msg set" |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
33 |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
34 |
translations |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
35 |
"spies" => "knows Spy" |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
36 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
37 |
|
11104 | 38 |
axioms |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset
|
39 |
(*Spy has access to his own key for spoof messages, but Server is secure*) |
11310 | 40 |
Spy_in_bad [iff] : "Spy \\<in> bad" |
41 |
Server_not_bad [iff] : "Server \\<notin> bad" |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
42 |
|
5183 | 43 |
primrec |
11104 | 44 |
knows_Nil: "knows A [] = initState A" |
45 |
knows_Cons: |
|
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
46 |
"knows A (ev # evs) = |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
47 |
(if A = Spy then |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
48 |
(case ev of |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
49 |
Says A' B X => insert X (knows Spy evs) |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
50 |
| Gets A' X => knows Spy evs |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
51 |
| Notes A' X => |
11310 | 52 |
if A' \\<in> bad then insert X (knows Spy evs) else knows Spy evs) |
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
53 |
else |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
54 |
(case ev of |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
55 |
Says A' B X => |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
56 |
if A'=A then insert X (knows A evs) else knows A evs |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
57 |
| Gets A' X => |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
58 |
if A'=A then insert X (knows A evs) else knows A evs |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
59 |
| Notes A' X => |
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset
|
60 |
if A'=A then insert X (knows A evs) else knows A evs))" |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
61 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
62 |
(* |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
63 |
Case A=Spy on the Gets event |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
64 |
enforces the fact that if a message is received then it must have been sent, |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
65 |
therefore the oops case must use Notes |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
66 |
*) |
3678 | 67 |
|
3683 | 68 |
consts |
69 |
(*Set of items that might be visible to somebody: |
|
70 |
complement of the set of fresh items*) |
|
11104 | 71 |
used :: "event list => msg set" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
72 |
|
5183 | 73 |
primrec |
11104 | 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))" |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
80 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset
|
81 |
|
11104 | 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)) *} |
|
11310 | 87 |
"for proving theorems of the form X \\<notin> analz (knows Spy evs) --> P" |
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
88 |
|
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset
|
89 |
end |