--- a/src/HOL/Auth/Public.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Public.thy Tue Feb 13 13:16:27 2001 +0100
@@ -8,30 +8,39 @@
Private and public keys; initial states of agents
*)
-Public = Event +
+theory Public = Event
+files ("Public_lemmas.ML"):
consts
- pubK :: agent => key
+ pubK :: "agent => key"
syntax
- priK :: agent => key
+ 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 =
+ initState_Server: "initState Server =
insert (Key (priK Server)) (Key ` range pubK)"
- initState_Friend "initState (Friend i) =
+ initState_Friend: "initState (Friend i) =
insert (Key (priK (Friend i))) (Key ` range pubK)"
- initState_Spy "initState Spy =
+ initState_Spy: "initState Spy =
(Key`invKey`pubK`bad) Un (Key ` range pubK)"
-rules
+axioms
(*Public keys are disjoint, and never clash with private keys*)
- inj_pubK "inj pubK"
- priK_neq_pubK "priK A ~= pubK B"
+ 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