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;


7 
Inductive relations "parts", "analyze" and "synthesize"


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 
(*We do not assume Crypt (Crypt X K) (invKey K) = X


32 
because Crypt is a constructor! We assume that encryption is injective,


33 
which is not true in the real world. The alternative is to take


34 
Crypt as an uninterpreted function symbol satisfying the equation


35 
above. This seems to require moving to ZF and regarding msg as an


36 
inductive definition instead of a datatype.*)


37 


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


39 
agent = Server  Friend nat  Enemy


40 


41 
consts


42 
isEnemy :: agent => bool


43 


44 
primrec isEnemy agent


45 
isEnemy_Server "isEnemy Server = False"


46 
isEnemy_Friend "isEnemy (Friend i) = False"


47 
isEnemy_Enemy "isEnemy Enemy = True"


48 


49 
datatype (*Messages are agent names, nonces, keys, pairs and encryptions*)


50 
msg = Agent agent


51 
 Nonce nat


52 
 Key key


53 
 MPair msg msg


54 
 Crypt msg key


55 


56 
(*Allows messages of the form {A,B,NA}, etc...*)


57 
syntax


58 
"@MTuple" :: "['a, args] => 'a * 'b" ("(1{_,/ _})")


59 


60 
translations


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


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


63 


64 


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


66 
keysFor :: msg set => key set


67 
"keysFor H == invKey `` {K. EX X. Crypt X K : H}"


68 


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


70 


71 
consts parts :: msg set => msg set


72 
inductive "parts H"


73 
intrs


74 
Inj "X: H ==> X: parts H"


75 
Fst "{X,Y} : parts H ==> X : parts H"


76 
Snd "{X,Y} : parts H ==> Y : parts H"


77 
Body "Crypt X K : parts H ==> X : parts H"


78 


79 


80 
(** Inductive definition of "analyze"  what can be broken down from a set of


81 
messages, including keys. A form of downward closure. Pairs can


82 
be taken apart; messages decrypted with known keys. **)


83 


84 
consts analyze :: msg set => msg set


85 
inductive "analyze H"


86 
intrs


87 
Inj "X: H ==> X: analyze H"


88 


89 
Fst "{X,Y} : analyze H ==> X : analyze H"


90 


91 
Snd "{X,Y} : analyze H ==> Y : analyze H"


92 


93 
Decrypt "[ Crypt X K : analyze H; Key(invKey K): analyze H


94 
] ==> X : analyze H"


95 


96 


97 
(** Inductive definition of "synthesize"  what can be built up from a set of


98 
messages. A form of upward closure. Pairs can be built, messages


99 
encrypted with known keys. Agent names may be quoted. **)


100 


101 
consts synthesize :: msg set => msg set


102 
inductive "synthesize H"


103 
intrs


104 
Inj "X: H ==> X: synthesize H"


105 


106 
Agent "Agent agt : synthesize H"


107 


108 
MPair "[ X: synthesize H; Y: synthesize H


109 
] ==> {X,Y} : synthesize H"


110 


111 
Crypt "[ X: synthesize H; Key(K): synthesize H


112 
] ==> Crypt X K : synthesize H"


113 


114 
end
