author  paulson 
Fri, 13 Dec 1996 10:17:35 +0100  
changeset 2373  490ffa16952e 
parent 2284  80ebd1a213fd 
child 2484  596a5b5a68ff 
permissions  rwrr 
1839  1 
(* Title: HOL/Auth/Message 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Datatypes of agents and messages; 

1913  7 
Inductive relations "parts", "analz" and "synth" 
1839  8 
*) 
9 

10 
Message = Arith + 

11 

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

13 
Do we need a type of nonces?*) 

14 

15 
types 

16 
key = nat 

17 

18 
consts 

19 
invKey :: key=>key 

20 

21 
rules 

22 
invKey "invKey (invKey K) = K" 

23 

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

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

26 

27 
constdefs 

28 
isSymKey :: key=>bool 

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

30 

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

2032  32 
agent = Server  Friend nat  Spy 
1839  33 

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

35 
msg = Agent agent 

36 
 Nonce nat 

37 
 Key key 

2373  38 
 Hash msg 
1839  39 
 MPair msg msg 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

40 
 Crypt key msg 
1839  41 

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

43 
syntax 

1947  44 
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})") 
1839  45 

46 
translations 

47 
"{x, y, z}" == "{x, {y, z}}" 

48 
"{x, y}" == "MPair x y" 

49 

50 

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

52 
keysFor :: msg set => key set 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

53 
"keysFor H == invKey `` {K. EX X. Crypt K X : H}" 
1839  54 

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

56 

57 
consts parts :: msg set => msg set 

58 
inductive "parts H" 

59 
intrs 

2373  60 
Inj "X: H ==> X: parts H" 
61 
Fst "{X,Y} : parts H ==> X : parts H" 

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

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

63 
Body "Crypt K X : parts H ==> X : parts H" 
1839  64 

65 

1913  66 
(** Inductive definition of "analz"  what can be broken down from a set of 
1839  67 
messages, including keys. A form of downward closure. Pairs can 
68 
be taken apart; messages decrypted with known keys. **) 

69 

1913  70 
consts analz :: msg set => msg set 
71 
inductive "analz H" 

1839  72 
intrs 
1913  73 
Inj "X: H ==> X: analz H" 
74 
Fst "{X,Y} : analz H ==> X : analz H" 

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

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

76 
Decrypt "[ Crypt K X : analz H; Key(invKey K): analz H ] ==> X : analz H" 
1839  77 

78 

1913  79 
(** Inductive definition of "synth"  what can be built up from a set of 
1839  80 
messages. A form of upward closure. Pairs can be built, messages 
81 
encrypted with known keys. Agent names may be quoted. **) 

82 

1913  83 
consts synth :: msg set => msg set 
84 
inductive "synth H" 

1839  85 
intrs 
1913  86 
Inj "X: H ==> X: synth H" 
87 
Agent "Agent agt : synth H" 

2373  88 
Hash "X: synth H ==> Hash X : synth H" 
1913  89 
MPair "[ X: synth H; Y: synth H ] ==> {X,Y} : synth H" 
2373  90 
Crypt "[ X: synth H; Key(K) : H ] ==> Crypt K X : synth H" 
1839  91 

92 
end 