diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Protocol/Event.thy --- a/src/Doc/Tutorial/Protocol/Event.thy Thu Jan 11 13:48:17 2018 +0100 +++ b/src/Doc/Tutorial/Protocol/Event.thy Fri Jan 12 14:08:53 2018 +0100 @@ -7,7 +7,7 @@ stores are visible to him *)(*<*) -section{*Theory of Events for Security Protocols*} +section\Theory of Events for Security Protocols\ theory Event imports Message begin @@ -20,10 +20,10 @@ | Notes agent msg consts - bad :: "agent set" -- {* compromised agents *} + bad :: "agent set" \ \compromised agents\ -text{*The constant "spies" is retained for compatibility's sake*} +text\The constant "spies" is retained for compatibility's sake\ primrec knows :: "agent => event list => msg set" @@ -50,7 +50,7 @@ spies :: "event list => msg set" where "spies == knows Spy" -text{*Spy has access to his own key for spoof messages, but Server is secure*} +text\Spy has access to his own key for spoof messages, but Server is secure\ specification (bad) Spy_in_bad [iff]: "Spy \ bad" Server_not_bad [iff]: "Server \ bad" @@ -73,9 +73,9 @@ Says A B X => parts {X} \ used evs | Gets A X => used evs | Notes A X => parts {X} \ used evs)" - --{*The case for @{term Gets} seems anomalous, but @{term Gets} always + \\The case for @{term Gets} seems anomalous, but @{term Gets} always follows @{term Says} in real protocols. Seems difficult to change. - See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *} + See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}.\ lemma Notes_imp_used [rule_format]: "Notes A X \ set evs --> X \ used evs" apply (induct_tac evs) @@ -88,7 +88,7 @@ done -subsection{*Function @{term knows}*} +subsection\Function @{term knows}\ (*Simplifying parts(insert X (knows Spy evs)) = parts{X} \ parts(knows Spy evs). @@ -99,8 +99,8 @@ "knows Spy (Says A B X # evs) = insert X (knows Spy evs)" by simp -text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits - on whether @{term "A=Spy"} and whether @{term "A\bad"}*} +text\Letting the Spy see "bad" agents' notes avoids redundant case-splits + on whether @{term "A=Spy"} and whether @{term "A\bad"}\ lemma knows_Spy_Notes [simp]: "knows Spy (Notes A X # evs) = (if A:bad then insert X (knows Spy evs) else knows Spy evs)" @@ -121,7 +121,7 @@ "knows Spy evs \ knows Spy (Gets A X # evs)" by (simp add: subset_insertI) -text{*Spy sees what is sent on the traffic*} +text\Spy sees what is sent on the traffic\ lemma Says_imp_knows_Spy [rule_format]: "Says A B X \ set evs --> X \ knows Spy evs" apply (induct_tac "evs") @@ -135,21 +135,21 @@ done -text{*Elimination rules: derive contradictions from old Says events containing - items known to be fresh*} +text\Elimination rules: derive contradictions from old Says events containing + items known to be fresh\ lemmas knows_Spy_partsEs = Says_imp_knows_Spy [THEN parts.Inj, elim_format] parts.Body [elim_format] lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj] -text{*Compatibility for the old "spies" function*} +text\Compatibility for the old "spies" function\ lemmas spies_partsEs = knows_Spy_partsEs lemmas Says_imp_spies = Says_imp_knows_Spy lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy] -subsection{*Knowledge of Agents*} +subsection\Knowledge of Agents\ lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)" by simp @@ -171,21 +171,21 @@ lemma knows_subset_knows_Gets: "knows A evs \ knows A (Gets A' X # evs)" by (simp add: subset_insertI) -text{*Agents know what they say*} +text\Agents know what they say\ lemma Says_imp_knows [rule_format]: "Says A B X \ set evs --> X \ knows A evs" apply (induct_tac "evs") apply (simp_all (no_asm_simp) split: event.split) apply blast done -text{*Agents know what they note*} +text\Agents know what they note\ lemma Notes_imp_knows [rule_format]: "Notes A X \ set evs --> X \ knows A evs" apply (induct_tac "evs") apply (simp_all (no_asm_simp) split: event.split) apply blast done -text{*Agents know what they receive*} +text\Agents know what they receive\ lemma Gets_imp_knows_agents [rule_format]: "A \ Spy --> Gets A X \ set evs --> X \ knows A evs" apply (induct_tac "evs") @@ -193,8 +193,8 @@ done -text{*What agents DIFFERENT FROM Spy know - was either said, or noted, or got, or known initially*} +text\What agents DIFFERENT FROM Spy know + was either said, or noted, or got, or known initially\ lemma knows_imp_Says_Gets_Notes_initState [rule_format]: "[| X \ knows A evs; A \ Spy |] ==> EX B. Says A B X \ set evs | Gets A X \ set evs | Notes A X \ set evs | X \ initState A" @@ -204,8 +204,8 @@ apply blast done -text{*What the Spy knows -- for the time being -- - was either said or noted, or known initially*} +text\What the Spy knows -- for the time being -- + was either said or noted, or known initially\ lemma knows_Spy_imp_Says_Notes_initState [rule_format]: "[| X \ knows Spy evs |] ==> EX A B. Says A B X \ set evs | Notes A X \ set evs | X \ initState Spy" @@ -241,15 +241,15 @@ apply (blast intro: initState_into_used) done -text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} +text\NOTE REMOVAL--laws above are cleaner, as they don't involve "case"\ declare knows_Cons [simp del] used_Nil [simp del] used_Cons [simp del] -text{*For proving theorems of the form @{term "X \ analz (knows Spy evs) --> P"} +text\For proving theorems of the form @{term "X \ analz (knows Spy evs) --> P"} New events added by induction to "evs" are discarded. Provided this information isn't needed, the proof will be much shorter, since - it will omit complicated reasoning about @{term analz}.*} + it will omit complicated reasoning about @{term analz}.\ lemmas analz_mono_contra = knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] @@ -259,12 +259,12 @@ lemmas analz_impI = impI [where P = "Y \ analz (knows Spy evs)"] for Y evs ML -{* +\ fun analz_mono_contra_tac ctxt = resolve_tac ctxt @{thms analz_impI} THEN' REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra}) THEN' mp_tac ctxt -*} +\ lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" by (induct e, auto simp: knows_Cons) @@ -275,7 +275,7 @@ done -text{*For proving @{text new_keys_not_used}*} +text\For proving @{text new_keys_not_used}\ lemma keysFor_parts_insert: "[| K \ keysFor (parts (insert X G)); X \ synth (analz H) |] ==> K \ keysFor (parts (G \ H)) | Key (invKey K) \ parts H" @@ -284,16 +284,16 @@ analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) -method_setup analz_mono_contra = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *} +method_setup analz_mono_contra = \ + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\ "for proving theorems of the form X \ analz (knows Spy evs) --> P" -subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} +subsubsection\Useful for case analysis on whether a hash is a spoof or not\ lemmas syan_impI = impI [where P = "Y \ synth (analz (knows Spy evs))"] for Y evs ML -{* +\ val knows_Cons = @{thm knows_Cons}; val used_Nil = @{thm used_Nil}; val used_Cons = @{thm used_Cons}; @@ -339,16 +339,16 @@ @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) THEN' mp_tac ctxt -*} +\ -method_setup synth_analz_mono_contra = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *} +method_setup synth_analz_mono_contra = \ + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt)))\ "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" (*>*) -section{* Event Traces \label{sec:events} *} +section\Event Traces \label{sec:events}\ -text {* +text \ The system's behaviour is formalized as a set of traces of \emph{events}. The most important event, @{text "Says A B X"}, expresses $A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$. @@ -379,7 +379,7 @@ \item @{term "synth (analz (knows Spy evs))"} is everything that the spy could generate \end{itemize} -*} +\ (*<*) end