1 (* Title: HOL/Auth/Message
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"
12 (*Is there a difference between a nonce and arbitrary numerical data?
13 Do we need a type of nonces?*)
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*)
29 "isSymKey K == (invKey K = K)"
31 datatype (*We allow any number of friendly agents*)
32 agent = Server | Friend nat | Spy
34 datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)
42 (*Allows messages of the form {|A,B,NA|}, etc...*)
44 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
47 "{|x, y, z|}" == "{|x, {|y, z|}|}"
48 "{|x, y|}" == "MPair x y"
52 (*Message Y, paired with a MAC computed with the help of X*)
53 HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000])
54 "Hash[X] Y == {| Hash{|X,Y|}, Y|}"
56 (*Keys useful to decrypt elements of a message set*)
57 keysFor :: msg set => key set
58 "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
60 (** Inductive definition of all "parts" of a message. **)
62 consts parts :: msg set => msg set
65 Inj "X: H ==> X: parts H"
66 Fst "{|X,Y|} : parts H ==> X : parts H"
67 Snd "{|X,Y|} : parts H ==> Y : parts H"
68 Body "Crypt K X : parts H ==> X : parts H"
71 (** Inductive definition of "analz" -- what can be broken down from a set of
72 messages, including keys. A form of downward closure. Pairs can
73 be taken apart; messages decrypted with known keys. **)
75 consts analz :: msg set => msg set
78 Inj "X: H ==> X: analz H"
79 Fst "{|X,Y|} : analz H ==> X : analz H"
80 Snd "{|X,Y|} : analz H ==> Y : analz H"
81 Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
84 (** Inductive definition of "synth" -- what can be built up from a set of
85 messages. A form of upward closure. Pairs can be built, messages
86 encrypted with known keys. Agent names may be quoted. **)
88 consts synth :: msg set => msg set
91 Inj "X: H ==> X: synth H"
92 Agent "Agent agt : synth H"
93 Hash "X: synth H ==> Hash X : 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"