# HG changeset patch # User wenzelm # Date 1298040373 -3600 # Node ID 13b97824aec6ef89b554fef254b6f586ebf35843 # Parent a710e96583d5358bfec5c7f31bd3fedafcd44be9 modernized specifications; diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/Guard/Proto.thy --- 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*} diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/KerberosIV.thy --- 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 \ bad" --{*Tgs is secure --- we already know that Kas is secure*} diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/KerberosIV_Gets.thy --- 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 \ bad" --{*Tgs is secure --- we already know that Kas is secure*} diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/KerberosV.thy --- 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 \ bad" --{*Tgs is secure --- we already know that Kas is secure*} diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/Message.thy --- 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 \ (B \ A) = B \ A" by blast -types +type_synonym key = nat consts diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/Public.thy --- 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 \ 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 \ symKeys" --{*All shared keys are symmetric*} text{*Injectiveness: Agents' long-term keys are distinct.*} diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/Smartcard/ShoupRubin.thy --- 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' \ k = k')" - + inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \ k = k')" and (*all long-term keys differ from sesK*) - shrK_disj_sesK [iff]: "shrK A \ sesK(m,pk)" - crdK_disj_sesK [iff]: "crdK C \ sesK(m,pk)" - pin_disj_sesK [iff]: "pin P \ sesK(m,pk)" - pairK_disj_sesK[iff]:"pairK(A,B) \ sesK(m,pk)" + shrK_disj_sesK [iff]: "shrK A \ sesK(m,pk)" and + crdK_disj_sesK [iff]: "crdK C \ sesK(m,pk)" and + pin_disj_sesK [iff]: "pin P \ sesK(m,pk)" and + pairK_disj_sesK[iff]:"pairK(A,B) \ sesK(m,pk)" and (*needed for base case in analz_image_freshK*) Atomic_distrib [iff]: "Atomic`(KEY`K \ NONCE`N) = - Atomic`(KEY`K) \ Atomic`(NONCE`N)" + Atomic`(KEY`K) \ Atomic`(NONCE`N)" and (*this protocol makes the assumption of secure means between each agent and his smartcard*) diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- 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' \ k = k')" + inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \ k = k')" and (*all long-term keys differ from sesK*) - shrK_disj_sesK [iff]: "shrK A \ sesK(m,pk)" - crdK_disj_sesK [iff]: "crdK C \ sesK(m,pk)" - pin_disj_sesK [iff]: "pin P \ sesK(m,pk)" - pairK_disj_sesK[iff]: "pairK(A,B) \ sesK(m,pk)" + shrK_disj_sesK [iff]: "shrK A \ sesK(m,pk)" and + crdK_disj_sesK [iff]: "crdK C \ sesK(m,pk)" and + pin_disj_sesK [iff]: "pin P \ sesK(m,pk)" and + pairK_disj_sesK[iff]: "pairK(A,B) \ sesK(m,pk)" and (*needed for base case in analz_image_freshK*) Atomic_distrib [iff]: "Atomic`(KEY`K \ NONCE`N) = - Atomic`(KEY`K) \ Atomic`(NONCE`N)" + Atomic`(KEY`K) \ Atomic`(NONCE`N)" and (*this protocol makes the assumption of secure means between each agent and his smartcard*) diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/Smartcard/Smartcard.thy --- 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) \ crdK C" - pairK_disj_shrK [iff]: "pairK(A,B) \ shrK P" - pairK_disj_pin [iff]: "pairK(A,B) \ pin P" - shrK_disj_crdK [iff]: "shrK P \ crdK C" - shrK_disj_pin [iff]: "shrK P \ pin Q" + pairK_disj_crdK [iff]: "pairK(A,B) \ crdK C" and + pairK_disj_shrK [iff]: "pairK(A,B) \ shrK P" and + pairK_disj_pin [iff]: "pairK(A,B) \ pin P" and + shrK_disj_crdK [iff]: "shrK P \ crdK C" and + shrK_disj_pin [iff]: "shrK P \ pin Q" and crdK_disj_pin [iff]: "crdK C \ pin P" definition legalUse :: "card => bool" ("legalUse (_)") where @@ -78,8 +77,8 @@ end text{*Still relying on axioms*} -axioms - Key_supply_ax: "finite KK \ \ K. K \ KK & Key K \ used evs" +axiomatization where + Key_supply_ax: "finite KK \ \ K. K \ KK & Key K \ used evs" and (*Needed because of Spy's knowledge of Pairkeys*) Nonce_supply_ax: "finite NN \ \ N. N \ NN & Nonce N \ used evs" @@ -129,7 +128,7 @@ (*Specialized to shared-key model: no @{term invKey}*) lemma keysFor_parts_insert: "\ K \ keysFor (parts (insert X G)); X \ synth (analz H) \ - \ K \ keysFor (parts (G \ H)) | Key K \ parts H"; + \ K \ keysFor (parts (G \ H)) | Key K \ parts H" by (force dest: EventSC.keysFor_parts_insert) lemma Crypt_imp_keysFor: "Crypt K X \ H \ K \ keysFor H" diff -r a710e96583d5 -r 13b97824aec6 src/HOL/Auth/TLS.thy --- 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 \ symKeys" + isSym_sessionK: "sessionK nonces \ symKeys" and --{*sessionK never clashes with a long-term symmetric key (they don't exist in TLS anyway)*}