Tidying and replacement of some axioms by specifications
authorpaulson
Thu Jul 24 16:36:29 2003 +0200 (2003-07-24)
changeset 1412628824746d046
parent 14125 bf8edef6c1f1
child 14127 40a4768c8e0b
Tidying and replacement of some axioms by specifications
src/HOL/Auth/Event.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/TLS.thy
src/HOL/ex/Puzzle.thy
     1.1 --- a/src/HOL/Auth/Event.thy	Thu Jul 24 16:35:51 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Jul 24 16:36:29 2003 +0200
     1.3 @@ -26,18 +26,21 @@
     1.4    knows  :: "agent => event list => msg set"
     1.5  
     1.6  
     1.7 -(*"spies" is retained for compatibility's sake*)
     1.8 +text{*The constant "spies" is retained for compatibility's sake*}
     1.9  syntax
    1.10    spies  :: "event list => msg set"
    1.11  
    1.12  translations
    1.13    "spies"   => "knows Spy"
    1.14  
    1.15 +text{*Spy has access to his own key for spoof messages, but Server is secure*}
    1.16 +specification (bad)
    1.17 +  bad_properties: "Spy \<in> bad & Server \<notin> bad"
    1.18 +    by (rule exI [of _ "{Spy}"], simp)
    1.19  
    1.20 -axioms
    1.21 -  (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.22 -  Spy_in_bad     [iff] :    "Spy \<in> bad"
    1.23 -  Server_not_bad [iff] : "Server \<notin> bad"
    1.24 +lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff]
    1.25 +lemmas Server_not_bad = bad_properties [THEN conjunct2, iff]
    1.26 +
    1.27  
    1.28  primrec
    1.29    knows_Nil:   "knows A [] = initState A"
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Thu Jul 24 16:35:51 2003 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu Jul 24 16:36:29 2003 +0200
     2.3 @@ -34,19 +34,23 @@
     2.4      (*Duration of the authenticator*)
     2.5      AutLife :: nat
     2.6  
     2.7 -axioms
     2.8 -    (*The ticket should remain fresh for two journeys on the network at least*)
     2.9 -    SesKeyLife_LB: "2 <= SesKeyLife"
    2.10 +text{*The ticket should remain fresh for two journeys on the network at least*}
    2.11 +specification (SesKeyLife)
    2.12 +  SesKeyLife_LB [iff]: "2 \<le> SesKeyLife"
    2.13 +    by blast
    2.14  
    2.15 -    (*The authenticator only for one journey*)
    2.16 -    AutLife_LB:    "Suc 0 <= AutLife"
    2.17 +text{*The authenticator only for one journey*}
    2.18 +specification (AutLife)
    2.19 +  AutLife_LB [iff]:    "Suc 0 \<le> AutLife"
    2.20 +    by blast
    2.21 +
    2.22  
    2.23  translations
    2.24     "CT" == "length"
    2.25    
    2.26     "Expired T evs" == "SesKeyLife + T < CT evs"
    2.27  
    2.28 -   "RecentAuth T evs" == "CT evs <= AutLife + T"
    2.29 +   "RecentAuth T evs" == "CT evs \<le> AutLife + T"
    2.30  
    2.31  consts  kerberos_ban   :: "event list set"
    2.32  inductive "kerberos_ban"
    2.33 @@ -100,9 +104,6 @@
    2.34  declare analz_subset_parts [THEN subsetD, dest]
    2.35  declare Fake_parts_insert [THEN subsetD, dest]
    2.36  
    2.37 -declare SesKeyLife_LB [iff] AutLife_LB [iff]
    2.38 -
    2.39 -
    2.40  (*A "possibility property": there are traces that reach the end.*)
    2.41  lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.     
    2.42               Says B A (Crypt K (Number Timestamp))  
    2.43 @@ -250,7 +251,7 @@
    2.44  
    2.45  lemma analz_image_freshK [rule_format (no_asm)]:
    2.46       "evs \<in> kerberos_ban ==>                           
    2.47 -   \<forall>K KK. KK <= - (range shrK) -->                  
    2.48 +   \<forall>K KK. KK \<subseteq> - (range shrK) -->                  
    2.49            (Key K \<in> analz (Key`KK Un (spies evs))) =   
    2.50            (K \<in> KK | Key K \<in> analz (spies evs))"
    2.51  apply (erule kerberos_ban.induct)
     3.1 --- a/src/HOL/Auth/Message.thy	Thu Jul 24 16:35:51 2003 +0200
     3.2 +++ b/src/HOL/Auth/Message.thy	Thu Jul 24 16:36:29 2003 +0200
     3.3 @@ -19,13 +19,20 @@
     3.4    key = nat
     3.5  
     3.6  consts
     3.7 -  invKey :: "key=>key"
     3.8 +  all_symmetric :: bool        --{*true if all keys are symmetric*}
     3.9 +  invKey        :: "key=>key"  --{*inverse of a symmetric key*}
    3.10 +
    3.11 +specification (invKey)
    3.12 +  invKey_cases: "(\<forall>K. invKey(invKey K) = K) & (all_symmetric --> invKey = id)"
    3.13 +    by (rule exI [of _ id], auto)
    3.14  
    3.15 -axioms
    3.16 -  invKey [simp] : "invKey (invKey K) = K"
    3.17 +
    3.18 +lemma invKey [simp]: "invKey (invKey K) = K"
    3.19 +by (simp add: invKey_cases)
    3.20  
    3.21 -  (*The inverse of a symmetric key is itself;
    3.22 -    that of a public key is the private key and vice versa*)
    3.23 +
    3.24 +text{*The inverse of a symmetric key is itself; that of a public key
    3.25 +      is the private key and vice versa*}
    3.26  
    3.27  constdefs
    3.28    symKeys :: "key set"
    3.29 @@ -764,7 +771,7 @@
    3.30  
    3.31  ML
    3.32  {*
    3.33 -(*ML bindings for definitions and axioms*)
    3.34 +(*ML bindings for definitions*)
    3.35  
    3.36  val invKey = thm "invKey"
    3.37  val keysFor_def = thm "keysFor_def"
     4.1 --- a/src/HOL/Auth/Public.thy	Thu Jul 24 16:35:51 2003 +0200
     4.2 +++ b/src/HOL/Auth/Public.thy	Thu Jul 24 16:36:29 2003 +0200
     4.3 @@ -45,12 +45,18 @@
     4.4    "priK A" == "invKey (pubEK A)"
     4.5  
     4.6  
     4.7 -axioms
     4.8 -  (*By freeness of agents, no two agents have the same key.  Since true\<noteq>false,
     4.9 -    no agent has identical signing and encryption keys*)
    4.10 +text{*By freeness of agents, no two agents have the same key.  Since
    4.11 +  @{term "True\<noteq>False"}, no agent has identical signing and encryption keys*}
    4.12 +specification (publicKey)
    4.13    injective_publicKey:
    4.14      "publicKey b A = publicKey c A' ==> b=c & A=A'"
    4.15 +   apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) 
    4.16 +   apply (auto simp add: inj_on_def split: agent.split) 
    4.17 +   apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
    4.18 +   done                       
    4.19  
    4.20 +
    4.21 +axioms
    4.22    (*No private key equals any public key (essential to ensure that private
    4.23      keys are private!) *)
    4.24    privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
    4.25 @@ -115,8 +121,14 @@
    4.26  consts
    4.27    shrK    :: "agent => key"    --{*long-term shared keys*}
    4.28  
    4.29 +specification (shrK)
    4.30 +  inj_shrK: "inj shrK"
    4.31 +  --{*No two agents have the same long-term key*}
    4.32 +   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
    4.33 +   apply (simp add: inj_on_def split: agent.split) 
    4.34 +   done
    4.35 +
    4.36  axioms
    4.37 -  inj_shrK: "inj shrK"	             --{*No two agents have the same key*}
    4.38    sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
    4.39  
    4.40  (*Injectiveness: Agents' long-term keys are distinct.*)
     5.1 --- a/src/HOL/Auth/Shared.thy	Thu Jul 24 16:35:51 2003 +0200
     5.2 +++ b/src/HOL/Auth/Shared.thy	Thu Jul 24 16:36:29 2003 +0200
     5.3 @@ -11,14 +11,24 @@
     5.4  theory Shared = Event:
     5.5  
     5.6  consts
     5.7 -  shrK    :: "agent => key"  (*symmetric keys*)
     5.8 +  shrK    :: "agent => key"  (*symmetric keys*);
     5.9 +
    5.10 +specification (shrK)
    5.11 +  inj_shrK: "inj shrK"
    5.12 +  --{*No two agents have the same long-term key*}
    5.13 +   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
    5.14 +   apply (simp add: inj_on_def split: agent.split) 
    5.15 +   done
    5.16  
    5.17 -axioms
    5.18 -  isSym_keys: "K \<in> symKeys"	(*All keys are symmetric*)
    5.19 -  inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
    5.20 +text{*All keys are symmetric*}
    5.21 +
    5.22 +defs  all_symmetric_def: "all_symmetric == True"
    5.23  
    5.24 +lemma isSym_keys: "K \<in> symKeys"	
    5.25 +by (simp add: symKeys_def all_symmetric_def invKey_cases) 
    5.26 +
    5.27 +text{*Server knows all long-term keys; other agents know only their own*}
    5.28  primrec
    5.29 -        (*Server knows all long-term keys; other agents know only their own*)
    5.30    initState_Server:  "initState Server     = Key ` range shrK"
    5.31    initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
    5.32    initState_Spy:     "initState Spy        = Key`shrK`bad"
     6.1 --- a/src/HOL/Auth/TLS.thy	Thu Jul 24 16:35:51 2003 +0200
     6.2 +++ b/src/HOL/Auth/TLS.thy	Thu Jul 24 16:36:29 2003 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4  
     6.5  header{*The TLS Protocol: Transport Layer Security*}
     6.6  
     6.7 -theory TLS = Public:
     6.8 +theory TLS = Public + NatPair:
     6.9  
    6.10  constdefs
    6.11    certificate      :: "[agent,key] => msg"
    6.12 @@ -71,13 +71,25 @@
    6.13    "clientK X" == "sessionK(X, ClientRole)"
    6.14    "serverK X" == "sessionK(X, ServerRole)"
    6.15  
    6.16 -axioms
    6.17 +specification (PRF)
    6.18 +  inj_PRF: "inj PRF"
    6.19    --{*the pseudo-random function is collision-free*}
    6.20 -  inj_PRF:       "inj PRF"
    6.21 +   apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"])
    6.22 +   apply (simp add: inj_on_def) 
    6.23 +   apply (blast dest!: nat2_to_nat_inj [THEN injD]) 
    6.24 +   done
    6.25  
    6.26 +specification (sessionK)
    6.27 +  inj_sessionK: "inj sessionK"
    6.28    --{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
    6.29 -  inj_sessionK:  "inj sessionK"	
    6.30 +   apply (rule exI [of _ 
    6.31 +         "%((x,y,z), r). nat2_to_nat(role_case 0 1 r, 
    6.32 +                           nat2_to_nat(x, nat2_to_nat(y,z)))"])
    6.33 +   apply (simp add: inj_on_def split: role.split) 
    6.34 +   apply (blast dest!: nat2_to_nat_inj [THEN injD]) 
    6.35 +   done
    6.36  
    6.37 +axioms
    6.38    --{*sessionK makes symmetric keys*}
    6.39    isSym_sessionK: "sessionK nonces \<in> symKeys"
    6.40  
     7.1 --- a/src/HOL/ex/Puzzle.thy	Thu Jul 24 16:35:51 2003 +0200
     7.2 +++ b/src/HOL/ex/Puzzle.thy	Thu Jul 24 16:36:29 2003 +0200
     7.3 @@ -12,7 +12,9 @@
     7.4  
     7.5  consts f :: "nat => nat"
     7.6  
     7.7 -axioms  f_ax [intro!]: "f(f(n)) < f(Suc(n))"
     7.8 +specification (f)
     7.9 +  f_ax [intro!]: "f(f(n)) < f(Suc(n))"
    7.10 +    by (rule exI [of _ id], simp)
    7.11  
    7.12  
    7.13  lemma lemma0 [rule_format]: "\<forall>n. k=f(n) --> n <= f(n)"