--- a/src/HOL/Auth/Shared.thy Mon Sep 21 15:33:39 2009 +0200
+++ b/src/HOL/Auth/Shared.thy Mon Sep 21 15:33:40 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Shared
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -8,7 +7,9 @@
Shared, long-term keys; initial states of agents
*)
-theory Shared imports Event begin
+theory Shared
+imports Event All_Symmetric
+begin
consts
shrK :: "agent => key" (*symmetric keys*);
@@ -20,13 +21,6 @@
apply (simp add: inj_on_def split: agent.split)
done
-text{*All keys are symmetric*}
-
-defs all_symmetric_def: "all_symmetric == True"
-
-lemma isSym_keys: "K \<in> symKeys"
-by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
-
text{*Server knows all long-term keys; other agents know only their own*}
primrec
initState_Server: "initState Server = Key ` range shrK"