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