author  paulson 
Fri, 16 Oct 1998 12:20:41 +0200  
changeset 5652  fe5f5510aef4 
parent 5234  701fa0ed77b7 
child 6807  6737af18317e 
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 

5234  31 

32 
(*Datatype msg is (awkwardly) split into two parts to avoid having freeness 

33 
expressed using natural numbers.*) 

3668  34 
datatype 
35 
atomic = AGENT agent (*Agent names*) 

36 
 NUMBER nat (*Ordinary integers, timestamps, ...*) 

37 
 NONCE nat (*Unguessable nonces*) 

38 
 KEY key (*Crypto keys*) 

39 

40 
datatype 

5234  41 
msg = Atomic atomic 
42 
 Hash msg (*Hashing*) 

43 
 MPair msg msg (*Compound messages*) 

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

1839  45 

5234  46 
(*These translations complete the illustion that "msg" has seven constructors*) 
1839  47 
syntax 
5234  48 
Agent :: agent => msg 
49 
Number :: nat => msg 

50 
Nonce :: nat => msg 

51 
Key :: key => msg 

52 

53 
translations 

54 
"Agent x" == "Atomic (AGENT x)" 

55 
"Number x" == "Atomic (NUMBER x)" 

56 
"Nonce x" == "Atomic (NONCE x)" 

57 
"Key x" == "Atomic (KEY x)" 

58 
"Key``x" == "Atomic `` (KEY `` x)" 

59 

60 

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

62 
syntax 

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

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

65 
translations 

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

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

68 

69 

2484  70 
constdefs 
71 
(*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

72 
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

73 
"Hash[X] Y == { Hash{X,Y}, Y}" 
2484  74 

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

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

77 
"keysFor H == invKey `` {K. EX X. Crypt K X : H}" 
1839  78 

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

80 

81 
consts parts :: msg set => msg set 

82 
inductive "parts H" 

83 
intrs 

2373  84 
Inj "X: H ==> X: parts H" 
85 
Fst "{X,Y} : parts H ==> X : parts H" 

86 
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

87 
Body "Crypt K X : parts H ==> X : parts H" 
1839  88 

89 

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

93 

1913  94 
consts analz :: msg set => msg set 
95 
inductive "analz H" 

1839  96 
intrs 
1913  97 
Inj "X: H ==> X: analz H" 
98 
Fst "{X,Y} : analz H ==> X : analz H" 

99 
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

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

102 

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

1839  107 

1913  108 
consts synth :: msg set => msg set 
109 
inductive "synth H" 

1839  110 
intrs 
1913  111 
Inj "X: H ==> X: synth H" 
112 
Agent "Agent agt : synth H" 

3668  113 
Number "Number n : synth H" 
2373  114 
Hash "X: synth H ==> Hash X : synth H" 
1913  115 
MPair "[ X: synth H; Y: synth H ] ==> {X,Y} : synth H" 
2373  116 
Crypt "[ X: synth H; Key(K) : H ] ==> Crypt K X : synth H" 
1839  117 

118 
end 