summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Auth/Message.thy

author | paulson |

Fri Nov 29 18:03:21 1996 +0100 (1996-11-29) | |

changeset 2284 | 80ebd1a213fd |

parent 2121 | 7e118eb32bdc |

child 2373 | 490ffa16952e |

permissions | -rw-r--r-- |

Swapped arguments of Crypt (for clarity and because it is conventional)

1 (* Title: HOL/Auth/Message

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1996 University of Cambridge

6 Datatypes of agents and messages;

7 Inductive relations "parts", "analz" and "synth"

8 *)

10 Message = Arith +

12 (*Is there a difference between a nonce and arbitrary numerical data?

13 Do we need a type of nonces?*)

15 types

16 key = nat

18 consts

19 invKey :: key=>key

21 rules

22 invKey "invKey (invKey K) = K"

24 (*The inverse of a symmetric key is itself;

25 that of a public key is the private key and vice versa*)

27 constdefs

28 isSymKey :: key=>bool

29 "isSymKey K == (invKey K = K)"

31 (*We do not assume Crypt (invKey K) (Crypt K X) = X

32 because Crypt a is constructor! We assume that encryption is injective,

33 which is not true in the real world. The alternative is to take

34 Crypt an as uninterpreted function symbol satisfying the equation

35 above. This seems to require moving to ZF and regarding msg as an

36 inductive definition instead of a datatype.*)

38 datatype (*We allow any number of friendly agents*)

39 agent = Server | Friend nat | Spy

41 datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)

42 msg = Agent agent

43 | Nonce nat

44 | Key key

45 | MPair msg msg

46 | Crypt key msg

48 (*Allows messages of the form {|A,B,NA|}, etc...*)

49 syntax

50 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")

52 translations

53 "{|x, y, z|}" == "{|x, {|y, z|}|}"

54 "{|x, y|}" == "MPair x y"

57 constdefs (*Keys useful to decrypt elements of a message set*)

58 keysFor :: msg set => key set

59 "keysFor H == invKey `` {K. EX X. Crypt K X : H}"

61 (** Inductive definition of all "parts" of a message. **)

63 consts parts :: msg set => msg set

64 inductive "parts H"

65 intrs

66 Inj "X: H ==> X: parts H"

67 Fst "{|X,Y|} : parts H ==> X : parts H"

68 Snd "{|X,Y|} : parts H ==> Y : parts H"

69 Body "Crypt K X : parts H ==> X : parts H"

72 (** Inductive definition of "analz" -- what can be broken down from a set of

73 messages, including keys. A form of downward closure. Pairs can

74 be taken apart; messages decrypted with known keys. **)

76 consts analz :: msg set => msg set

77 inductive "analz H"

78 intrs

79 Inj "X: H ==> X: analz H"

80 Fst "{|X,Y|} : analz H ==> X : analz H"

81 Snd "{|X,Y|} : analz H ==> Y : analz H"

82 Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"

85 (** Inductive definition of "synth" -- what can be built up from a set of

86 messages. A form of upward closure. Pairs can be built, messages

87 encrypted with known keys. Agent names may be quoted. **)

89 consts synth :: msg set => msg set

90 inductive "synth H"

91 intrs

92 Inj "X: H ==> X: synth H"

93 Agent "Agent agt : synth H"

94 MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H"

95 Crypt "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"

97 end