# HG changeset patch
# User haftmann
# Date 1253540020 -7200
# Node ID 2489e3c3562bc16ce5213392183929cfb10d765d
# Parent  133e4a6474e3f29e3aeca00d245df13ec8725c48
common base for protocols with symmetric keys

diff -r 133e4a6474e3 -r 2489e3c3562b src/HOL/Auth/All_Symmetric.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/All_Symmetric.thy	Mon Sep 21 15:33:40 2009 +0200
@@ -0,0 +1,12 @@
+theory All_Symmetric
+imports Message
+begin
+
+text {* All keys are symmetric *}
+
+defs all_symmetric_def: "all_symmetric \<equiv> True"
+
+lemma isSym_keys: "K \<in> symKeys"
+  by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
+
+end
diff -r 133e4a6474e3 -r 2489e3c3562b src/HOL/Auth/Shared.thy
--- 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"
diff -r 133e4a6474e3 -r 2489e3c3562b src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Sep 21 15:33:39 2009 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Sep 21 15:33:40 2009 +0200
@@ -1,10 +1,11 @@
-(*  ID:         $Id$
-    Author:     Giampaolo Bella, Catania University
+(* Author:     Giampaolo Bella, Catania University
 *)
 
 header{*Theory of smartcards*}
 
-theory Smartcard imports EventSC begin
+theory Smartcard
+imports EventSC All_Symmetric
+begin
 
 text{*  
 As smartcards handle long-term (symmetric) keys, this theoy extends and 
@@ -42,14 +43,6 @@
   shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q"
   crdK_disj_pin [iff]:   "crdK C \<noteq> pin P"
 
-
-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) 
-
-
 constdefs
   legalUse :: "card => bool" ("legalUse (_)")
   "legalUse C == C \<notin> stolen"