author  paulson 
Thu, 10 Jun 1999 10:36:41 +0200  
changeset 6807  6737af18317e 
parent 5652  fe5f5510aef4 
child 7057  b9ddbb925939 
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)" 

6807  57 
"Nonce``x" == "Atomic `` (NONCE `` x)" 
5234  58 
"Key x" == "Atomic (KEY x)" 
59 
"Key``x" == "Atomic `` (KEY `` x)" 

60 

61 

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

63 
syntax 

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

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

66 
translations 

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

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

69 

70 

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

73 
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

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

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

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

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

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

81 

82 
consts parts :: msg set => msg set 

83 
inductive "parts H" 

84 
intrs 

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

87 
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

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

90 

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

94 

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

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

100 
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

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

103 

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

1839  108 

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

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

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

119 
end 