(*  Title:      HOL/Auth/Public

     ID:         $Id$

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     Copyright   1996  University of Cambridge

 Theory of Public Keys (common to all public-key protocols)

 Private and public keys; initial states of agents

 *)

 theory Public = Event

 files ("Public_lemmas.ML"):

 consts

   pubK    :: "agent => key"

 syntax

   priK    :: "agent => key"

 translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)

   "priK x"  == "invKey(pubK x)"

 primrec

         (*Agents know their private key and all public keys*)

   initState_Server:  "initState Server     =    

  		         insert (Key (priK Server)) (Key ` range pubK)"

   initState_Friend:  "initState (Friend i) =    

  		         insert (Key (priK (Friend i))) (Key ` range pubK)"

   initState_Spy:     "initState Spy        =    

  		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"

 axioms

   (*Public keys are disjoint, and never clash with private keys*)

   inj_pubK:        "inj pubK"

   priK_neq_pubK:   "priK A ~= pubK B"

 use "Public_lemmas.ML"

 (*Specialized methods*)

 method_setup possibility = {*

     Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}

     "for proving possibility theorems"

 end