--- a/src/HOL/Auth/Public.thy Wed Jul 09 17:00:34 1997 +0200
+++ b/src/HOL/Auth/Public.thy Fri Jul 11 13:26:15 1997 +0200
@@ -3,12 +3,12 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-Theory of Public Keys (common to all symmetric-key protocols)
+Theory of Public Keys (common to all public-key protocols)
-Server keys; initial states of agents; new nonces and keys; function "sees"
+Private and public keys; initial states of agents
*)
-Public = Message + List +
+Public = Event +
consts
pubK :: agent => key
@@ -19,9 +19,6 @@
translations (*BEWARE! expressions like (inj priK) will NOT work!*)
"priK x" == "invKey(pubK x)"
-consts (*Initial states of agents -- parameter of the construction*)
- initState :: [agent set, agent] => msg set
-
primrec initState agent
(*Agents know their private key and all public keys*)
initState_Server "initState lost Server =
@@ -32,31 +29,6 @@
(Key``invKey``pubK``lost) Un (Key `` range pubK)"
-datatype (*Messages, and components of agent stores*)
- event = Says agent agent msg
-
-consts
- sees1 :: [agent, event] => msg set
-
-primrec sees1 event
- (*Spy reads all traffic whether addressed to him or not*)
- sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})"
-
-consts
- sees :: [agent set, agent, event list] => msg set
-
-primrec sees list
- sees_Nil "sees lost A [] = initState lost A"
- sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-
-
-constdefs
- (*Set of items that might be visible to somebody: complement of the set
- of fresh items*)
- used :: event list => msg set
- "used evs == parts (UN lost B. sees lost B evs)"
-
-
rules
(*Public keys are disjoint, and never clash with private keys*)
inj_pubK "inj pubK"