# HG changeset patch # User paulson # Date 1059057389 -7200 # Node ID 28824746d04645c553f7e4cdc5aa9bc5883485c8 # Parent bf8edef6c1f1be9bbb719ce4b970cb2a6523ce15 Tidying and replacement of some axioms by specifications diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/Auth/Event.thy Thu Jul 24 16:36:29 2003 +0200 @@ -26,18 +26,21 @@ knows :: "agent => event list => msg set" -(*"spies" is retained for compatibility's sake*) +text{*The constant "spies" is retained for compatibility's sake*} syntax spies :: "event list => msg set" translations "spies" => "knows Spy" +text{*Spy has access to his own key for spoof messages, but Server is secure*} +specification (bad) + bad_properties: "Spy \ bad & Server \ bad" + by (rule exI [of _ "{Spy}"], simp) -axioms - (*Spy has access to his own key for spoof messages, but Server is secure*) - Spy_in_bad [iff] : "Spy \ bad" - Server_not_bad [iff] : "Server \ bad" +lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff] +lemmas Server_not_bad = bad_properties [THEN conjunct2, iff] + primrec knows_Nil: "knows A [] = initState A" diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Jul 24 16:36:29 2003 +0200 @@ -34,19 +34,23 @@ (*Duration of the authenticator*) AutLife :: nat -axioms - (*The ticket should remain fresh for two journeys on the network at least*) - SesKeyLife_LB: "2 <= SesKeyLife" +text{*The ticket should remain fresh for two journeys on the network at least*} +specification (SesKeyLife) + SesKeyLife_LB [iff]: "2 \ SesKeyLife" + by blast - (*The authenticator only for one journey*) - AutLife_LB: "Suc 0 <= AutLife" +text{*The authenticator only for one journey*} +specification (AutLife) + AutLife_LB [iff]: "Suc 0 \ AutLife" + by blast + translations "CT" == "length" "Expired T evs" == "SesKeyLife + T < CT evs" - "RecentAuth T evs" == "CT evs <= AutLife + T" + "RecentAuth T evs" == "CT evs \ AutLife + T" consts kerberos_ban :: "event list set" inductive "kerberos_ban" @@ -100,9 +104,6 @@ declare analz_subset_parts [THEN subsetD, dest] declare Fake_parts_insert [THEN subsetD, dest] -declare SesKeyLife_LB [iff] AutLife_LB [iff] - - (*A "possibility property": there are traces that reach the end.*) lemma "\Timestamp K. \evs \ kerberos_ban. Says B A (Crypt K (Number Timestamp)) @@ -250,7 +251,7 @@ lemma analz_image_freshK [rule_format (no_asm)]: "evs \ kerberos_ban ==> - \K KK. KK <= - (range shrK) --> + \K KK. KK \ - (range shrK) --> (Key K \ analz (Key`KK Un (spies evs))) = (K \ KK | Key K \ analz (spies evs))" apply (erule kerberos_ban.induct) diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/Auth/Message.thy Thu Jul 24 16:36:29 2003 +0200 @@ -19,13 +19,20 @@ key = nat consts - invKey :: "key=>key" + all_symmetric :: bool --{*true if all keys are symmetric*} + invKey :: "key=>key" --{*inverse of a symmetric key*} + +specification (invKey) + invKey_cases: "(\K. invKey(invKey K) = K) & (all_symmetric --> invKey = id)" + by (rule exI [of _ id], auto) -axioms - invKey [simp] : "invKey (invKey K) = K" + +lemma invKey [simp]: "invKey (invKey K) = K" +by (simp add: invKey_cases) - (*The inverse of a symmetric key is itself; - that of a public key is the private key and vice versa*) + +text{*The inverse of a symmetric key is itself; that of a public key + is the private key and vice versa*} constdefs symKeys :: "key set" @@ -764,7 +771,7 @@ ML {* -(*ML bindings for definitions and axioms*) +(*ML bindings for definitions*) val invKey = thm "invKey" val keysFor_def = thm "keysFor_def" diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/Auth/Public.thy Thu Jul 24 16:36:29 2003 +0200 @@ -45,12 +45,18 @@ "priK A" == "invKey (pubEK A)" -axioms - (*By freeness of agents, no two agents have the same key. Since true\false, - no agent has identical signing and encryption keys*) +text{*By freeness of agents, no two agents have the same key. Since + @{term "True\False"}, no agent has identical signing and encryption keys*} +specification (publicKey) injective_publicKey: "publicKey b A = publicKey c A' ==> b=c & A=A'" + apply (rule exI [of _ "%b A. 2 * agent_case 0 (\n. n + 2) 1 A + (if b then 1 else 0)"]) + apply (auto simp add: inj_on_def split: agent.split) + apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ + done + +axioms (*No private key equals any public key (essential to ensure that private keys are private!) *) privateKey_neq_publicKey [iff]: "privateKey b A \ publicKey c A'" @@ -115,8 +121,14 @@ consts shrK :: "agent => key" --{*long-term shared keys*} +specification (shrK) + inj_shrK: "inj shrK" + --{*No two agents have the same long-term key*} + apply (rule exI [of _ "agent_case 0 (\n. n + 2) 1"]) + apply (simp add: inj_on_def split: agent.split) + done + axioms - inj_shrK: "inj shrK" --{*No two agents have the same key*} sym_shrK [iff]: "shrK X \ symKeys" --{*All shared keys are symmetric*} (*Injectiveness: Agents' long-term keys are distinct.*) diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/Auth/Shared.thy Thu Jul 24 16:36:29 2003 +0200 @@ -11,14 +11,24 @@ theory Shared = Event: consts - shrK :: "agent => key" (*symmetric keys*) + shrK :: "agent => key" (*symmetric keys*); + +specification (shrK) + inj_shrK: "inj shrK" + --{*No two agents have the same long-term key*} + apply (rule exI [of _ "agent_case 0 (\n. n + 2) 1"]) + apply (simp add: inj_on_def split: agent.split) + done -axioms - isSym_keys: "K \ symKeys" (*All keys are symmetric*) - inj_shrK: "inj shrK" (*No two agents have the same long-term key*) +text{*All keys are symmetric*} + +defs all_symmetric_def: "all_symmetric == True" +lemma isSym_keys: "K \ symKeys" +by (simp add: symKeys_def all_symmetric_def invKey_cases) + +text{*Server knows all long-term keys; other agents know only their own*} primrec - (*Server knows all long-term keys; other agents know only their own*) initState_Server: "initState Server = Key ` range shrK" initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}" initState_Spy: "initState Spy = Key`shrK`bad" diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/Auth/TLS.thy Thu Jul 24 16:36:29 2003 +0200 @@ -41,7 +41,7 @@ header{*The TLS Protocol: Transport Layer Security*} -theory TLS = Public: +theory TLS = Public + NatPair: constdefs certificate :: "[agent,key] => msg" @@ -71,13 +71,25 @@ "clientK X" == "sessionK(X, ClientRole)" "serverK X" == "sessionK(X, ServerRole)" -axioms +specification (PRF) + inj_PRF: "inj PRF" --{*the pseudo-random function is collision-free*} - inj_PRF: "inj PRF" + apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"]) + apply (simp add: inj_on_def) + apply (blast dest!: nat2_to_nat_inj [THEN injD]) + done +specification (sessionK) + inj_sessionK: "inj sessionK" --{*sessionK is collision-free; also, no clientK clashes with any serverK.*} - inj_sessionK: "inj sessionK" + apply (rule exI [of _ + "%((x,y,z), r). nat2_to_nat(role_case 0 1 r, + nat2_to_nat(x, nat2_to_nat(y,z)))"]) + apply (simp add: inj_on_def split: role.split) + apply (blast dest!: nat2_to_nat_inj [THEN injD]) + done +axioms --{*sessionK makes symmetric keys*} isSym_sessionK: "sessionK nonces \ symKeys" diff -r bf8edef6c1f1 -r 28824746d046 src/HOL/ex/Puzzle.thy --- a/src/HOL/ex/Puzzle.thy Thu Jul 24 16:35:51 2003 +0200 +++ b/src/HOL/ex/Puzzle.thy Thu Jul 24 16:36:29 2003 +0200 @@ -12,7 +12,9 @@ consts f :: "nat => nat" -axioms f_ax [intro!]: "f(f(n)) < f(Suc(n))" +specification (f) + f_ax [intro!]: "f(f(n)) < f(Suc(n))" + by (rule exI [of _ id], simp) lemma lemma0 [rule_format]: "\n. k=f(n) --> n <= f(n)"