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