--- 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 \<in> bad & Server \<notin> 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 \<in> bad"
- Server_not_bad [iff] : "Server \<notin> 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"
--- 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 \<le> 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 \<le> 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 \<le> 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 "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.
Says B A (Crypt K (Number Timestamp))
@@ -250,7 +251,7 @@
lemma analz_image_freshK [rule_format (no_asm)]:
"evs \<in> kerberos_ban ==>
- \<forall>K KK. KK <= - (range shrK) -->
+ \<forall>K KK. KK \<subseteq> - (range shrK) -->
(Key K \<in> analz (Key`KK Un (spies evs))) =
(K \<in> KK | Key K \<in> analz (spies evs))"
apply (erule kerberos_ban.induct)
--- 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: "(\<forall>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"
--- 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\<noteq>false,
- no agent has identical signing and encryption keys*)
+text{*By freeness of agents, no two agents have the same key. Since
+ @{term "True\<noteq>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 (\<lambda>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 \<noteq> 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 (\<lambda>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 \<in> symKeys" --{*All shared keys are symmetric*}
(*Injectiveness: Agents' long-term keys are distinct.*)
--- 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 (\<lambda>n. n + 2) 1"])
+ apply (simp add: inj_on_def split: agent.split)
+ done
-axioms
- isSym_keys: "K \<in> 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 \<in> 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"
--- 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 \<in> symKeys"
--- 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]: "\<forall>n. k=f(n) --> n <= f(n)"