Tidied. New Pi-theorem.
(* 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