--- a/src/HOL/Auth/Guard/Proto.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Fri Feb 18 15:46:13 2011 +0100
@@ -15,13 +15,13 @@
subsection{*protocols*}
-types rule = "event set * event"
+type_synonym rule = "event set * event"
abbreviation
msg' :: "rule => msg" where
"msg' R == msg (snd R)"
-types proto = "rule set"
+type_synonym proto = "rule set"
definition wdef :: "proto => bool" where
"wdef p == ALL R k. R:p --> Number k:parts {msg' R}
@@ -155,9 +155,9 @@
subsection{*types*}
-types keyfun = "rule => subs => nat => event list => key set"
+type_synonym keyfun = "rule => subs => nat => event list => key set"
-types secfun = "rule => nat => subs => key set => msg"
+type_synonym secfun = "rule => nat => subs => key set => msg"
subsection{*introduction of a fresh guarded nonce*}
--- a/src/HOL/Auth/KerberosIV.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Fri Feb 18 15:46:13 2011 +0100
@@ -16,7 +16,7 @@
Tgs :: agent where "Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/KerberosIV_Gets.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Fri Feb 18 15:46:13 2011 +0100
@@ -16,7 +16,7 @@
Tgs :: agent where "Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/KerberosV.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/KerberosV.thy Fri Feb 18 15:46:13 2011 +0100
@@ -17,7 +17,7 @@
"Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/Message.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/Message.thy Fri Feb 18 15:46:13 2011 +0100
@@ -16,7 +16,7 @@
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
by blast
-types
+type_synonym
key = nat
consts
--- a/src/HOL/Auth/Public.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/Public.thy Fri Feb 18 15:46:13 2011 +0100
@@ -68,7 +68,7 @@
done
-axioms
+axiomatization where
(*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'"
@@ -141,7 +141,7 @@
apply (simp add: inj_on_def split: agent.split)
done
-axioms
+axiomatization where
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
text{*Injectiveness: Agents' long-term keys are distinct.*}
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Fri Feb 18 15:46:13 2011 +0100
@@ -5,24 +5,19 @@
theory ShoupRubin imports Smartcard begin
-consts
-
- sesK :: "nat*key => key"
-
-axioms
-
+axiomatization sesK :: "nat*key => key"
+where
(*sesK is injective on each component*)
- inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
-
+ inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
(*all long-term keys differ from sesK*)
- shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
- crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
- pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
- pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)"
+ shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+ crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+ pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)" and
+ pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)" and
(*needed for base case in analz_image_freshK*)
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
- Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
+ Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
(*this protocol makes the assumption of secure means
between each agent and his smartcard*)
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Fri Feb 18 15:46:13 2011 +0100
@@ -11,24 +11,20 @@
Availability. Only the updated version makes the goals of confidentiality,
authentication and key distribution available to both peers.*}
-consts
-
- sesK :: "nat*key => key"
-
-axioms
-
+axiomatization sesK :: "nat*key => key"
+where
(*sesK is injective on each component*)
- inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
+ inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
(*all long-term keys differ from sesK*)
- shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
- crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
- pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
- pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)"
+ shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+ crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+ pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)" and
+ pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)" and
(*needed for base case in analz_image_freshK*)
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
- Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
+ Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
(*this protocol makes the assumption of secure means
between each agent and his smartcard*)
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Fri Feb 18 15:46:13 2011 +0100
@@ -16,31 +16,30 @@
smartcard, which independently may be stolen or cloned.
*}
-consts
- shrK :: "agent => key" (*long-term keys saved in smart cards*)
- crdK :: "card => key" (*smart cards' symmetric keys*)
- pin :: "agent => key" (*pin to activate the smart cards*)
+axiomatization
+ shrK :: "agent => key" and (*long-term keys saved in smart cards*)
+ crdK :: "card => key" and (*smart cards' symmetric keys*)
+ pin :: "agent => key" and (*pin to activate the smart cards*)
(*Mostly for Shoup-Rubin*)
- Pairkey :: "agent * agent => nat"
+ Pairkey :: "agent * agent => nat" and
pairK :: "agent * agent => key"
-
-axioms
- inj_shrK: "inj shrK" --{*No two smartcards store the same key*}
- inj_crdK: "inj crdK" --{*Nor do two cards*}
- inj_pin : "inj pin" --{*Nor do two agents have the same pin*}
+where
+ inj_shrK: "inj shrK" and --{*No two smartcards store the same key*}
+ inj_crdK: "inj crdK" and --{*Nor do two cards*}
+ inj_pin : "inj pin" and --{*Nor do two agents have the same pin*}
(*pairK is injective on each component, if we assume encryption to be a PRF
or at least collision free *)
- inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
- comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
+ inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')" and
+ comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)" and
(*long-term keys differ from each other*)
- pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
- pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
- pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P"
- shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C"
- shrK_disj_pin [iff]: "shrK P \<noteq> pin Q"
+ pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C" and
+ pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P" and
+ pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P" and
+ shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C" and
+ shrK_disj_pin [iff]: "shrK P \<noteq> pin Q" and
crdK_disj_pin [iff]: "crdK C \<noteq> pin P"
definition legalUse :: "card => bool" ("legalUse (_)") where
@@ -78,8 +77,8 @@
end
text{*Still relying on axioms*}
-axioms
- Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
+axiomatization where
+ Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs" and
(*Needed because of Spy's knowledge of Pairkeys*)
Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
@@ -129,7 +128,7 @@
(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
"\<lbrakk> K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) \<rbrakk>
- \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+ \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
by (force dest: EventSC.keysFor_parts_insert)
lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
--- a/src/HOL/Auth/TLS.thy Fri Feb 18 15:17:39 2011 +0100
+++ b/src/HOL/Auth/TLS.thy Fri Feb 18 15:46:13 2011 +0100
@@ -86,9 +86,9 @@
apply (simp add: inj_on_def prod_encode_eq split: role.split)
done
-axioms
+axiomatization where
--{*sessionK makes symmetric keys*}
- isSym_sessionK: "sessionK nonces \<in> symKeys"
+ isSym_sessionK: "sessionK nonces \<in> symKeys" and
--{*sessionK never clashes with a long-term symmetric key
(they don't exist in TLS anyway)*}