author  paulson 
Mon, 14 Jul 1997 12:47:21 +0200  
changeset 3519  ab0a9fbed4c0 
parent 3512  9dcb4daa15e8 
child 3678  414e04d7c2d6 
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 

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 (*Messagescould 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 