--- /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
--- 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"
--- 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"