diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/SET_Protocol/Message_SET.thy Thu May 26 17:51:22 2016 +0200 @@ -4,29 +4,29 @@ Author: Lawrence C Paulson *) -section{*The Message Theory, Modified for SET*} +section\The Message Theory, Modified for SET\ theory Message_SET imports Main "~~/src/HOL/Library/Nat_Bijection" begin -subsection{*General Lemmas*} +subsection\General Lemmas\ -text{*Needed occasionally with @{text spy_analz_tac}, e.g. in - @{text analz_insert_Key_newK}*} +text\Needed occasionally with \spy_analz_tac\, e.g. in + \analz_insert_Key_newK\\ lemma Un_absorb3 [simp] : "A \ (B \ A) = B \ A" by blast -text{*Collapses redundant cases in the huge protocol proofs*} +text\Collapses redundant cases in the huge protocol proofs\ lemmas disj_simps = disj_comms disj_left_absorb disj_assoc -text{*Effective with assumptions like @{term "K \ range pubK"} and - @{term "K \ invKey`range pubK"}*} +text\Effective with assumptions like @{term "K \ range pubK"} and + @{term "K \ invKey`range pubK"}\ lemma notin_image_iff: "(y \ f`I) = (\i\I. f i \ y)" by blast -text{*Effective with the assumption @{term "KK \ - (range(invKey o pubK))"} *} +text\Effective with the assumption @{term "KK \ - (range(invKey o pubK))"}\ lemma disjoint_image_iff: "(A <= - (f`I)) = (\i\I. f i \ A)" by blast @@ -35,8 +35,8 @@ type_synonym key = nat consts - all_symmetric :: bool --{*true if all keys are symmetric*} - invKey :: "key=>key" --{*inverse of a symmetric key*} + all_symmetric :: bool \\true if all keys are symmetric\ + invKey :: "key=>key" \\inverse of a symmetric key\ specification (invKey) invKey [simp]: "invKey (invKey K) = K" @@ -44,27 +44,27 @@ by (rule exI [of _ id], auto) -text{*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\ definition symKeys :: "key set" where "symKeys == {K. invKey K = K}" -text{*Agents. We allow any number of certification authorities, cardholders - merchants, and payment gateways.*} +text\Agents. We allow any number of certification authorities, cardholders + merchants, and payment gateways.\ datatype agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy -text{*Messages*} +text\Messages\ datatype - msg = Agent agent --{*Agent names*} - | Number nat --{*Ordinary integers, timestamps, ...*} - | Nonce nat --{*Unguessable nonces*} - | Pan nat --{*Unguessable Primary Account Numbers (??)*} - | Key key --{*Crypto keys*} - | Hash msg --{*Hashing*} - | MPair msg msg --{*Compound messages*} - | Crypt key msg --{*Encryption, public- or shared-key*} + msg = Agent agent \\Agent names\ + | Number nat \\Ordinary integers, timestamps, ...\ + | Nonce nat \\Unguessable nonces\ + | Pan nat \\Unguessable Primary Account Numbers (??)\ + | Key key \\Crypto keys\ + | Hash msg \\Hashing\ + | MPair msg msg \\Compound messages\ + | Crypt key msg \\Encryption, public- or shared-key\ (*Concrete syntax: messages appear as \\A,B,NA\\, etc...*) @@ -81,9 +81,9 @@ (curry prod_encode 2) (curry prod_encode 3) (prod_encode (4,0))" - --{*maps each agent to a unique natural number, for specifications*} + \\maps each agent to a unique natural number, for specifications\ -text{*The function is indeed injective*} +text\The function is indeed injective\ lemma inj_nat_of_agent: "inj nat_of_agent" by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) @@ -93,7 +93,7 @@ keysFor :: "msg set => key set" where "keysFor H = invKey ` {K. \X. Crypt K X \ H}" -subsubsection{*Inductive definition of all "parts" of a message.*} +subsubsection\Inductive definition of all "parts" of a message.\ inductive_set parts :: "msg set => msg set" @@ -113,7 +113,7 @@ done -subsubsection{*Inverse of keys*} +subsubsection\Inverse of keys\ (*Equations hold because constructors are injective; cannot prove for all f*) lemma Key_image_eq [simp]: "(Key x \ Key`A) = (x\A)" @@ -143,7 +143,7 @@ done -subsection{*keysFor operator*} +subsection\keysFor operator\ lemma keysFor_empty [simp]: "keysFor {} = {}" by (unfold keysFor_def, blast) @@ -190,7 +190,7 @@ by (unfold keysFor_def, blast) -subsection{*Inductive relation "parts"*} +subsection\Inductive relation "parts"\ lemma MPair_parts: "[| \X,Y\ \ parts H; @@ -198,10 +198,10 @@ by (blast dest: parts.Fst parts.Snd) declare MPair_parts [elim!] parts.Body [dest!] -text{*NB These two rules are UNSAFE in the formal sense, as they discard the +text\NB These two rules are UNSAFE in the formal sense, as they discard the compound message. They work well on THIS FILE. - @{text MPair_parts} is left as SAFE because it speeds up proofs. - The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*} + \MPair_parts\ is left as SAFE because it speeds up proofs. + The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\ lemma parts_increasing: "H \ parts(H)" by blast @@ -221,7 +221,7 @@ by (erule parts.induct, fast+) -subsubsection{*Unions*} +subsubsection\Unions\ lemma parts_Un_subset1: "parts(G) \ parts(H) \ parts(G \ H)" by (intro Un_least parts_mono Un_upper1 Un_upper2) @@ -262,15 +262,15 @@ NOTE: the UN versions are no longer used!*) -text{*This allows @{text blast} to simplify occurrences of - @{term "parts(G\H)"} in the assumption.*} +text\This allows \blast\ to simplify occurrences of + @{term "parts(G\H)"} in the assumption.\ declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!] lemma parts_insert_subset: "insert X (parts H) \ parts(insert X H)" by (blast intro: parts_mono [THEN [2] rev_subsetD]) -subsubsection{*Idempotence and transitivity*} +subsubsection\Idempotence and transitivity\ lemma parts_partsD [dest!]: "X\ parts (parts H) ==> X\ parts H" by (erule parts.induct, blast+) @@ -290,7 +290,7 @@ by (force dest!: parts_cut intro: parts_insertI) -subsubsection{*Rewrite rules for pulling out atomic messages*} +subsubsection\Rewrite rules for pulling out atomic messages\ lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] @@ -383,11 +383,11 @@ apply (rule_tac x = "N + Suc nat" in exI, auto) done -subsection{*Inductive relation "analz"*} +subsection\Inductive relation "analz"\ -text{*Inductive definition of "analz" -- what can be broken down from a set of +text\Inductive definition of "analz" -- what can be broken down from a set of messages, including keys. A form of downward closure. Pairs can - be taken apart; messages decrypted with known keys.*} + be taken apart; messages decrypted with known keys.\ inductive_set analz :: "msg set => msg set" @@ -407,7 +407,7 @@ apply (auto dest: Fst Snd) done -text{*Making it safe speeds up proofs*} +text\Making it safe speeds up proofs\ lemma MPair_analz [elim!]: "[| \X,Y\ \ analz H; [| X \ analz H; Y \ analz H |] ==> P @@ -440,7 +440,7 @@ lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD] -subsubsection{*General equational properties*} +subsubsection\General equational properties\ lemma analz_empty [simp]: "analz{} = {}" apply safe @@ -455,7 +455,7 @@ lemma analz_insert: "insert X (analz H) \ analz(insert X H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) -subsubsection{*Rewrite rules for pulling out atomic messages*} +subsubsection\Rewrite rules for pulling out atomic messages\ lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] @@ -568,7 +568,7 @@ done -subsubsection{*Idempotence and transitivity*} +subsubsection\Idempotence and transitivity\ lemma analz_analzD [dest!]: "X\ analz (analz H) ==> X\ analz H" by (erule analz.induct, blast+) @@ -594,7 +594,7 @@ by (blast intro: analz_cut analz_insertI) -text{*A congruence rule for "analz"*} +text\A congruence rule for "analz"\ lemma analz_subset_cong: "[| analz G \ analz G'; analz H \ analz H' @@ -631,12 +631,12 @@ by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD]) -subsection{*Inductive relation "synth"*} +subsection\Inductive relation "synth"\ -text{*Inductive definition of "synth" -- what can be built up from a set of +text\Inductive definition of "synth" -- what can be built up from a set of messages. A form of upward closure. Pairs can be built, messages encrypted with known keys. Agent names are public domain. - Numbers can be guessed, but Nonces cannot be.*} + Numbers can be guessed, but Nonces cannot be.\ inductive_set synth :: "msg set => msg set" @@ -668,7 +668,7 @@ lemma synth_increasing: "H \ synth(H)" by blast -subsubsection{*Unions*} +subsubsection\Unions\ (*Converse fails: we can synth more from the union than from the separate parts, building a compound message using elements of each.*) @@ -678,7 +678,7 @@ lemma synth_insert: "insert X (synth H) \ synth(insert X H)" by (blast intro: synth_mono [THEN [2] rev_subsetD]) -subsubsection{*Idempotence and transitivity*} +subsubsection\Idempotence and transitivity\ lemma synth_synthD [dest!]: "X\ synth (synth H) ==> X\ synth H" by (erule synth.induct, blast+) @@ -716,7 +716,7 @@ by (unfold keysFor_def, blast) -subsubsection{*Combinations of parts, analz and synth*} +subsubsection\Combinations of parts, analz and synth\ lemma parts_synth [simp]: "parts (synth H) = parts H \ synth H" apply (rule equalityI) @@ -745,7 +745,7 @@ done -subsubsection{*For reasoning about the Fake rule in traces*} +subsubsection\For reasoning about the Fake rule in traces\ lemma parts_insert_subset_Un: "X\ G ==> parts(insert X H) \ parts G \ parts H" by (rule subset_trans [OF parts_mono parts_Un_subset2], blast) @@ -806,8 +806,8 @@ declare parts.Body [rule del] -text{*Rewrites to push in Key and Crypt messages, so that other messages can - be pulled out using the @{text analz_insert} rules*} +text\Rewrites to push in Key and Crypt messages, so that other messages can + be pulled out using the \analz_insert\ rules\ lemmas pushKeys = insert_commute [of "Key K" "Agent C"] @@ -828,15 +828,15 @@ insert_commute [of "Crypt X K" "MPair X' Y"] for X K C N PAN X' Y -text{*Cannot be added with @{text "[simp]"} -- messages should not always be - re-ordered.*} +text\Cannot be added with \[simp]\ -- messages should not always be + re-ordered.\ lemmas pushes = pushKeys pushCrypts -subsection{*Tactics useful for many protocol proofs*} +subsection\Tactics useful for many protocol proofs\ (*<*) ML -{* +\ (*Analysis of Fake cases. Also works for messages that forward unknown parts, but this application is no longer necessary if analz_insert_eq is used. DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) @@ -873,7 +873,7 @@ simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); -*} +\ (*>*) @@ -901,7 +901,7 @@ apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) done -text{*Two generalizations of @{text analz_insert_eq}*} +text\Two generalizations of \analz_insert_eq\\ lemma gen_analz_insert_eq [rule_format]: "X \ analz H ==> ALL G. H \ G --> analz (insert X G) = analz G" by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD]) @@ -922,16 +922,16 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] -method_setup spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *} +method_setup spy_analz = \ + Scan.succeed (SIMPLE_METHOD' o spy_analz_tac)\ "for proving the Fake case when analz is involved" -method_setup atomic_spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *} +method_setup atomic_spy_analz = \ + Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac)\ "for debugging spy_analz" -method_setup Fake_insert_simp = {* - Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac) *} +method_setup Fake_insert_simp = \ + Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac)\ "for debugging spy_analz" end