diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Metis_Examples/Message.thy Thu May 26 17:51:22 2016 +0200 @@ -5,7 +5,7 @@ Metis example featuring message authentication. *) -section {* Metis Example Featuring Message Authentication *} +section \Metis Example Featuring Message Authentication\ theory Message imports Main @@ -19,8 +19,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" @@ -28,26 +28,26 @@ by (metis id_apply) -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}" -datatype --{*We allow any number of friendly agents*} +datatype \\We allow any number of friendly agents\ agent = Server | Friend nat | Spy datatype - msg = Agent agent --{*Agent names*} - | Number nat --{*Ordinary integers, timestamps, ...*} - | Nonce nat --{*Unguessable nonces*} - | 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\ + | Key key \\Crypto keys\ + | Hash msg \\Hashing\ + | MPair msg msg \\Compound messages\ + | Crypt key msg \\Encryption, public- or shared-key\ -text{*Concrete syntax: messages appear as \\A,B,NA\\, etc...*} +text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") translations @@ -56,15 +56,15 @@ definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where - --{*Message Y paired with a MAC computed with the help of X*} + \\Message Y paired with a MAC computed with the help of X\ "Hash[X] Y == \ Hash\X,Y\, Y\" definition keysFor :: "msg set => key set" where - --{*Keys useful to decrypt elements of a message set*} + \\Keys useful to decrypt elements of a message set\ "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" @@ -83,7 +83,7 @@ apply (metis parts.Snd) by (metis parts.Body) -text{*Equations hold because constructors are injective.*} +text\Equations hold because constructors are injective.\ lemma Friend_image_eq [simp]: "(Friend x \ Friend`A) = (x:A)" by (metis agent.inject image_iff) @@ -94,13 +94,13 @@ by (metis image_iff msg.distinct(23)) -subsubsection{*Inverse of keys *} +subsubsection\Inverse of keys\ lemma invKey_eq [simp]: "(invKey K = invKey K') = (K = K')" by (metis invKey) -subsection{*keysFor operator*} +subsection\keysFor operator\ lemma keysFor_empty [simp]: "keysFor {} = {}" by (unfold keysFor_def, blast) @@ -111,7 +111,7 @@ lemma keysFor_UN [simp]: "keysFor (\i\A. H i) = (\i\A. keysFor (H i))" by (unfold keysFor_def, blast) -text{*Monotonicity*} +text\Monotonicity\ lemma keysFor_mono: "G \ H ==> keysFor(G) \ keysFor(H)" by (unfold keysFor_def, blast) @@ -144,7 +144,7 @@ by (unfold keysFor_def, blast) -subsection{*Inductive relation "parts"*} +subsection\Inductive relation "parts"\ lemma MPair_parts: "[| \X,Y\ \ parts H; @@ -152,10 +152,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 @@ -171,14 +171,14 @@ lemma parts_emptyE [elim!]: "X\ parts{} ==> P" by simp -text{*WARNING: loops if H = {Y}, therefore must not be repeated!*} +text\WARNING: loops if H = {Y}, therefore must not be repeated!\ lemma parts_singleton: "X\ parts H ==> \Y\H. X\ parts {Y}" apply (erule parts.induct) apply fast+ done -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) @@ -212,19 +212,19 @@ lemma parts_UN [simp]: "parts(\x\A. H x) = (\x\A. parts(H x))" by (intro equalityI parts_UN_subset1 parts_UN_subset2) -text{*Added to simplify arguments to parts, analz and synth. - NOTE: the UN versions are no longer used!*} +text\Added to simplify arguments to parts, analz and synth. + 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.\ lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] declare in_parts_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+) @@ -245,7 +245,7 @@ by (metis (no_types) Un_insert_left Un_insert_right insert_absorb le_supE parts_Un parts_idem parts_increasing parts_trans) -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] @@ -310,11 +310,11 @@ apply (metis le_trans linorder_linear) 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" @@ -327,14 +327,14 @@ "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" -text{*Monotonicity; Lemma 1 of Lowe's paper*} +text\Monotonicity; Lemma 1 of Lowe's paper\ lemma analz_mono: "G\H ==> analz(G) \ analz(H)" apply auto apply (erule analz.induct) apply (auto dest: analz.Fst analz.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 @@ -367,22 +367,22 @@ 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 apply (erule analz.induct, blast+) done -text{*Converse fails: we can analz more from the union than from the - separate parts, as a key in one might decrypt a message in the other*} +text\Converse fails: we can analz more from the union than from the + separate parts, as a key in one might decrypt a message in the other\ lemma analz_Un: "analz(G) \ analz(H) \ analz(G \ H)" by (intro Un_least analz_mono Un_upper1 Un_upper2) 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] @@ -410,7 +410,7 @@ apply (erule analz.induct, auto) done -text{*Can only pull out Keys if they are not needed to decrypt the rest*} +text\Can only pull out Keys if they are not needed to decrypt the rest\ lemma analz_insert_Key [simp]: "K \ keysFor (analz H) ==> analz (insert (Key K) H) = insert (Key K) (analz H)" @@ -429,7 +429,7 @@ apply (blast intro: analz.Fst analz.Snd)+ done -text{*Can pull out enCrypted message if the Key is not known*} +text\Can pull out enCrypted message if the Key is not known\ lemma analz_insert_Crypt: "Key (invKey K) \ analz H ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" @@ -459,10 +459,10 @@ insert (Crypt K X) (analz (insert X H))" by (intro equalityI lemma1 lemma2) -text{*Case analysis: either the message is secure, or it is not! Effective, -but can cause subgoals to blow up! Use with @{text "if_split"}; apparently -@{text "split_tac"} does not cope with patterns such as @{term"analz (insert -(Crypt K X) H)"} *} +text\Case analysis: either the message is secure, or it is not! Effective, +but can cause subgoals to blow up! Use with \if_split\; apparently +\split_tac\ does not cope with patterns such as @{term"analz (insert +(Crypt K X) H)"}\ lemma analz_Crypt_if [simp]: "analz (insert (Crypt K X) H) = (if (Key (invKey K) \ analz H) @@ -471,7 +471,7 @@ by (simp add: analz_insert_Crypt analz_insert_Decrypt) -text{*This rule supposes "for the sake of argument" that we have the key.*} +text\This rule supposes "for the sake of argument" that we have the key.\ lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" @@ -486,7 +486,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+) @@ -509,14 +509,14 @@ lemma analz_cut: "[| Y\ analz (insert X H); X\ analz H |] ==> Y\ analz H" by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) -text{*This rewrite rule helps in the simplification of messages that involve +text\This rewrite rule helps in the simplification of messages that involve the forwarding of unknown components (X). Without it, removing occurrences - of X can be very complicated. *} + of X can be very complicated.\ lemma analz_insert_eq: "X\ analz H ==> analz (insert X H) = analz H" 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' |] @@ -535,14 +535,14 @@ "analz H = analz H' ==> analz(insert X H) = analz(insert X H')" by (force simp only: insert_def intro!: analz_cong) -text{*If there are no pairs or encryptions then analz does nothing*} +text\If there are no pairs or encryptions then analz does nothing\ lemma analz_trivial: "[| \X Y. \X,Y\ \ H; \X K. Crypt K X \ H |] ==> analz H = H" apply safe apply (erule analz.induct, blast+) done -text{*These two are obsolete (with a single Spy) but cost little to prove...*} +text\These two are obsolete (with a single Spy) but cost little to prove...\ lemma analz_UN_analz_lemma: "X\ analz (\i\A. analz (H i)) ==> X\ analz (\i\A. H i)" apply (erule analz.induct) @@ -553,12 +553,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" @@ -571,12 +571,12 @@ | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> \X,Y\ \ synth H" | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" -text{*Monotonicity*} +text\Monotonicity\ lemma synth_mono: "G\H ==> synth(G) \ synth(H)" by (auto, erule synth.induct, auto) -text{*NO @{text Agent_synth}, as any Agent name can be synthesized. - The same holds for @{term Number}*} +text\NO \Agent_synth\, as any Agent name can be synthesized. + The same holds for @{term Number}\ inductive_cases Nonce_synth [elim!]: "Nonce n \ synth H" inductive_cases Key_synth [elim!]: "Key K \ synth H" inductive_cases Hash_synth [elim!]: "Hash X \ synth H" @@ -587,17 +587,17 @@ lemma synth_increasing: "H \ synth(H)" by blast -subsubsection{*Unions *} +subsubsection\Unions\ -text{*Converse fails: we can synth more from the union than from the - separate parts, building a compound message using elements of each.*} +text\Converse fails: we can synth more from the union than from the + separate parts, building a compound message using elements of each.\ lemma synth_Un: "synth(G) \ synth(H) \ synth(G \ H)" by (intro Un_least synth_mono Un_upper1 Un_upper2) lemma synth_insert: "insert X (synth H) \ synth(insert X H)" by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono) -subsubsection{*Idempotence and transitivity *} +subsubsection\Idempotence and transitivity\ lemma synth_synthD [dest!]: "X\ synth (synth H) ==> X\ synth H" by (erule synth.induct, blast+) @@ -639,7 +639,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) @@ -681,7 +681,7 @@ qed -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" proof -