src/HOL/Auth/Message.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Message.thy	Fri Jun 28 15:26:39 1996 +0200
@@ -0,0 +1,114 @@
+(*  Title:      HOL/Auth/Message
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Datatypes of agents and messages;
+Inductive relations "parts", "analyze" and "synthesize"
+*)
+
+Message = Arith +
+
+(*Is there a difference between a nonce and arbitrary numerical data?
+  Do we need a type of nonces?*)
+
+types 
+  key = nat
+
+consts
+  invKey :: key=>key
+
+rules
+  invKey "invKey (invKey K) = K"
+
+  (*The inverse of a symmetric key is itself;
+    that of a public key is the private key and vice versa*)
+
+constdefs
+  isSymKey :: key=>bool
+  "isSymKey K == (invKey K = K)"
+
+  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
+    because Crypt is a constructor!  We assume that encryption is injective,
+    which is not true in the real world.  The alternative is to take
+    Crypt as an uninterpreted function symbol satisfying the equation
+    above.  This seems to require moving to ZF and regarding msg as an
+    inductive definition instead of a datatype.*) 
+
+datatype  (*We allow any number of friendly agents*)
+  agent = Server | Friend nat | Enemy
+
+consts  
+  isEnemy :: agent => bool
+
+primrec isEnemy agent
+  isEnemy_Server  "isEnemy Server  = False"
+  isEnemy_Friend  "isEnemy (Friend i) = False"
+  isEnemy_Enemy   "isEnemy Enemy = True"
+
+datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
+  msg = Agent agent
+      | Nonce nat
+      | Key   key
+      | MPair msg msg
+      | Crypt msg key
+
+(*Allows messages of the form {|A,B,NA|}, etc...*)
+syntax
+  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
+
+translations
+  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
+  "{|x, y|}"      == "MPair x y"
+
+
+constdefs  (*Keys useful to decrypt elements of a message set*)
+  keysFor :: msg set => key set
+  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
+
+(** Inductive definition of all "parts" of a message.  **)
+
+consts  parts   :: msg set => msg set
+inductive "parts H"
+  intrs 
+    Inj     "X: H ==> X: parts H"
+    Fst     "{|X,Y|} : parts H ==> X : parts H"
+    Snd     "{|X,Y|} : parts H ==> Y : parts H"
+    Body    "Crypt X K : parts H ==> X : parts H"
+
+
+(** Inductive definition of "analyze" -- what can be broken down from a set of
+    messages, including keys.  A form of downward closure.  Pairs can
+    be taken apart; messages decrypted with known keys.  **)
+
+consts  analyze   :: msg set => msg set
+inductive "analyze H"
+  intrs 
+    Inj     "X: H ==> X: analyze H"
+
+    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
+
+    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
+
+    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
+             |] ==> X : analyze H"
+
+
+(** Inductive definition of "synthesize" -- what can be built up from a set of
+    messages.  A form of upward closure.  Pairs can be built, messages
+    encrypted with known keys.  Agent names may be quoted.  **)
+
+consts  synthesize   :: msg set => msg set
+inductive "synthesize H"
+  intrs 
+    Inj     "X: H ==> X: synthesize H"
+
+    Agent   "Agent agt : synthesize H"
+
+    MPair   "[| X: synthesize H;  Y: synthesize H
+             |] ==> {|X,Y|} : synthesize H"
+
+    Crypt   "[| X: synthesize H; Key(K): synthesize H
+             |] ==> Crypt X K : synthesize H"
+
+end