author  paulson 
Thu, 18 Mar 1999 10:41:00 +0100  
changeset 6399  4a9040b85e2e 
parent 6308  76f3865a2b1d 
child 11104  f2024fed9f0c 
permissions  rwrr 
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 

6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

19 
datatype 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

20 
event = Says agent agent msg 
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

21 
 Gets agent msg 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

22 
 Notes agent msg 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

23 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

24 
consts 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

25 
bad :: agent set (*compromised agents*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

26 
knows :: agent => event list => msg set 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

27 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

28 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

29 
(*"spies" is retained for compability's sake*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

30 
syntax 
3683  31 
spies :: event list => msg set 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

32 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

33 
translations 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

34 
"spies" => "knows Spy" 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

35 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

36 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

37 
rules 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

38 
(*Spy has access to his own key for spoof messages, but Server is secure*) 
3683  39 
Spy_in_bad "Spy: bad" 
40 
Server_not_bad "Server ~: bad" 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

41 

5183  42 
primrec 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

43 
knows_Nil "knows A [] = initState A" 
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

44 
knows_Cons 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

45 
"knows A (ev # evs) = 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

46 
(if A = Spy then 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

47 
(case ev of 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

48 
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

49 
 Gets A' X => knows Spy evs 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

50 
 Notes A' X => 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

51 
if A' : bad then insert X (knows Spy evs) else knows Spy evs) 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

52 
else 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

53 
(case ev of 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

54 
Says A' B X => 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

55 
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

56 
 Gets A' X => 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

57 
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

58 
 Notes A' X => 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

59 
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

60 

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 
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

63 
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

64 
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

65 
*) 
3678  66 

3683  67 
consts 
68 
(*Set of items that might be visible to somebody: 

69 
complement of the set of fresh items*) 

70 
used :: event list => msg set 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

71 

5183  72 
primrec 
3683  73 
used_Nil "used [] = (UN B. parts (initState B))" 
74 
used_Cons "used (ev # evs) = 

75 
(case ev of 

76 
Says A B X => parts {X} Un (used evs) 

6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

77 
 Gets A X => used evs 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

78 
 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

79 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5183
diff
changeset

80 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

81 

9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

82 
end 