author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 2516  4d68fbe6378b 
child 3668  a39baf59ea47 
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 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

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 

2484  51 
constdefs 
52 
(*Message Y, paired with a MAC computed with the help of X*) 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

53 
HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000]) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

54 
"Hash[X] Y == { Hash{X,Y}, Y}" 
2484  55 

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

1839  57 
keysFor :: msg set => key set 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

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

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

61 

62 
consts parts :: msg set => msg set 

63 
inductive "parts H" 

64 
intrs 

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

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

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

70 

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

74 

1913  75 
consts analz :: msg set => msg set 
76 
inductive "analz H" 

1839  77 
intrs 
1913  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" 

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

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

83 

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

87 

1913  88 
consts synth :: msg set => msg set 
89 
inductive "synth H" 

1839  90 
intrs 
1913  91 
Inj "X: H ==> X: synth H" 
92 
Agent "Agent agt : synth H" 

2373  93 
Hash "X: synth H ==> Hash X : synth H" 
1913  94 
MPair "[ X: synth H; Y: synth H ] ==> {X,Y} : synth H" 
2373  95 
Crypt "[ X: synth H; Key(K) : H ] ==> Crypt K X : synth H" 
1839  96 

97 
end 