common base for protocols with symmetric keys
authorhaftmann
Mon Sep 21 15:33:40 2009 +0200 (2009-09-21)
changeset 326312489e3c3562b
parent 32630 133e4a6474e3
child 32632 8ae912371831
common base for protocols with symmetric keys
src/HOL/Auth/All_Symmetric.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/Smartcard.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/All_Symmetric.thy	Mon Sep 21 15:33:40 2009 +0200
     1.3 @@ -0,0 +1,12 @@
     1.4 +theory All_Symmetric
     1.5 +imports Message
     1.6 +begin
     1.7 +
     1.8 +text {* All keys are symmetric *}
     1.9 +
    1.10 +defs all_symmetric_def: "all_symmetric \<equiv> True"
    1.11 +
    1.12 +lemma isSym_keys: "K \<in> symKeys"
    1.13 +  by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    1.14 +
    1.15 +end
     2.1 --- a/src/HOL/Auth/Shared.thy	Mon Sep 21 15:33:39 2009 +0200
     2.2 +++ b/src/HOL/Auth/Shared.thy	Mon Sep 21 15:33:40 2009 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Auth/Shared
     2.5 -    ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   1996  University of Cambridge
     2.8  
     2.9 @@ -8,7 +7,9 @@
    2.10  Shared, long-term keys; initial states of agents
    2.11  *)
    2.12  
    2.13 -theory Shared imports Event begin
    2.14 +theory Shared
    2.15 +imports Event All_Symmetric
    2.16 +begin
    2.17  
    2.18  consts
    2.19    shrK    :: "agent => key"  (*symmetric keys*);
    2.20 @@ -20,13 +21,6 @@
    2.21     apply (simp add: inj_on_def split: agent.split) 
    2.22     done
    2.23  
    2.24 -text{*All keys are symmetric*}
    2.25 -
    2.26 -defs  all_symmetric_def: "all_symmetric == True"
    2.27 -
    2.28 -lemma isSym_keys: "K \<in> symKeys"	
    2.29 -by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    2.30 -
    2.31  text{*Server knows all long-term keys; other agents know only their own*}
    2.32  primrec
    2.33    initState_Server:  "initState Server     = Key ` range shrK"
     3.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Sep 21 15:33:39 2009 +0200
     3.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Sep 21 15:33:40 2009 +0200
     3.3 @@ -1,10 +1,11 @@
     3.4 -(*  ID:         $Id$
     3.5 -    Author:     Giampaolo Bella, Catania University
     3.6 +(* Author:     Giampaolo Bella, Catania University
     3.7  *)
     3.8  
     3.9  header{*Theory of smartcards*}
    3.10  
    3.11 -theory Smartcard imports EventSC begin
    3.12 +theory Smartcard
    3.13 +imports EventSC All_Symmetric
    3.14 +begin
    3.15  
    3.16  text{*  
    3.17  As smartcards handle long-term (symmetric) keys, this theoy extends and 
    3.18 @@ -42,14 +43,6 @@
    3.19    shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q"
    3.20    crdK_disj_pin [iff]:   "crdK C \<noteq> pin P"
    3.21  
    3.22 -
    3.23 -text{*All keys are symmetric*}
    3.24 -defs  all_symmetric_def: "all_symmetric == True"
    3.25 -
    3.26 -lemma isSym_keys: "K \<in> symKeys"	
    3.27 -by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    3.28 -
    3.29 -
    3.30  constdefs
    3.31    legalUse :: "card => bool" ("legalUse (_)")
    3.32    "legalUse C == C \<notin> stolen"