author  paulson 
Wed, 21 Jul 1999 15:22:11 +0200  
changeset 7057  b9ddbb925939 
parent 6807  6737af18317e 
child 9686  87b460d72e80 
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 

5652  10 
Message = Main + 
1839  11 

12 
types 

13 
key = nat 

14 

15 
consts 

16 
invKey :: key=>key 

17 

18 
rules 

19 
invKey "invKey (invKey K) = K" 

20 

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

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

23 

24 
constdefs 

25 
isSymKey :: key=>bool 

26 
"isSymKey K == (invKey K = K)" 

27 

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

2032  29 
agent = Server  Friend nat  Spy 
1839  30 

3668  31 
datatype 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

32 
msg = Agent agent (*Agent names*) 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

33 
 Number nat (*Ordinary integers, timestamps, ...*) 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

34 
 Nonce nat (*Unguessable nonces*) 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

35 
 Key key (*Crypto keys*) 
5234  36 
 Hash msg (*Hashing*) 
37 
 MPair msg msg (*Compound messages*) 

38 
 Crypt key msg (*Encryption, public or sharedkey*) 

1839  39 

5234  40 

41 
(*Concrete syntax: messages appear as {A,B,NA}, etc...*) 

42 
syntax 

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

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

45 
translations 

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

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

48 

49 

2484  50 
constdefs 
51 
(*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

52 
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

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

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

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

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

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

60 

61 
consts parts :: msg set => msg set 

62 
inductive "parts H" 

63 
intrs 

2373  64 
Inj "X: H ==> X: parts H" 
65 
Fst "{X,Y} : parts H ==> X : parts H" 

66 
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

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

69 

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

73 

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

1839  76 
intrs 
1913  77 
Inj "X: H ==> X: analz H" 
78 
Fst "{X,Y} : analz H ==> X : analz H" 

79 
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

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

82 

1913  83 
(** Inductive definition of "synth"  what can be built up from a set of 
1839  84 
messages. A form of upward closure. Pairs can be built, messages 
3668  85 
encrypted with known keys. Agent names are public domain. 
86 
Numbers can be guessed, but Nonces cannot be. **) 

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

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

98 
end 