Moving common declarations and proofs from theories "Shared"
and "Public" to "Event". NB the original "Event" theory was later renamed "Shared".
Addition of the Notes constructor to datatype "event".
(* 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
*)
Public = Event +
consts
pubK :: agent => key
syntax
priK :: agent => key
translations (*BEWARE! expressions like (inj priK) will NOT work!*)
"priK x" == "invKey(pubK x)"
primrec initState agent
(*Agents know their private key and all public keys*)
initState_Server "initState lost Server =
insert (Key (priK Server)) (Key `` range pubK)"
initState_Friend "initState lost (Friend i) =
insert (Key (priK (Friend i))) (Key `` range pubK)"
initState_Spy "initState lost Spy =
(Key``invKey``pubK``lost) Un (Key `` range pubK)"
rules
(*Public keys are disjoint, and never clash with private keys*)
inj_pubK "inj pubK"
priK_neq_pubK "priK A ~= pubK B"
end