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 


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

1947

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

1839

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 

1913

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

1839

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


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


83 

1913

84 
consts analz :: msg set => msg set


85 
inductive "analz H"

1839

86 
intrs

1913

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


88 
Fst "{X,Y} : analz H ==> X : analz H"


89 
Snd "{X,Y} : analz H ==> Y : analz H"


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

1839

91 


92 

1913

93 
(** Inductive definition of "synth"  what can be built up from a set of

1839

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


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


96 

1913

97 
consts synth :: msg set => msg set


98 
inductive "synth H"

1839

99 
intrs

1913

100 
Inj "X: H ==> X: synth H"


101 
Agent "Agent agt : synth H"


102 
MPair "[ X: synth H; Y: synth H ] ==> {X,Y} : synth H"


103 
Crypt "[ X: synth H; Key(K): synth H ] ==> Crypt X K : synth H"

1839

104 


105 
end
