# HG changeset patch # User berghofe # Date 1185193894 -7200 # Node ID ee98c2528a8f25807850d3217abe48f5dd2489a5 # Parent 883359757a560920dd217f38b1004a127577fc65 LaTeX code is now generated directly from theory files. diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Mon Jul 23 14:30:53 2007 +0200 +++ b/doc-src/TutorialI/Protocol/Event.thy Mon Jul 23 14:31:34 2007 +0200 @@ -3,16 +3,15 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge -Theory of events for security protocols - Datatype of events; function "spies"; freshness "bad" agents have been broken by the Spy; their private keys and internal stores are visible to him -*) +*)(*<*) -theory Event imports Message -uses ("Event_lemmas.ML") begin +header{*Theory of Events for Security Protocols*} + +theory Event imports Message begin consts (*Initial states of agents -- parameter of the construction*) initState :: "agent => msg set" @@ -27,18 +26,17 @@ knows :: "agent => event list => msg set" -(*"spies" is retained for compatibility's sake*) -syntax - spies :: "event list => msg set" +text{*The constant "spies" is retained for compatibility's sake*} + +abbreviation (input) + spies :: "event list => msg set" where + "spies == knows Spy" -translations - "spies" => "knows Spy" - - -axioms - (*Spy has access to his own key for spoof messages, but Server is secure*) - Spy_in_bad [iff] : "Spy \ bad" - Server_not_bad [iff] : "Server \ bad" +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" + by (rule exI [of _ "{Spy}"], simp) primrec knows_Nil: "knows A [] = initState A" @@ -74,16 +72,321 @@ used_Nil: "used [] = (UN B. parts (initState B))" used_Cons: "used (ev # evs) = (case ev of - Says A B X => parts {X} Un (used evs) + Says A B X => parts {X} \ used evs | Gets A X => used evs - | Notes A X => parts {X} Un (used evs))" + | Notes A X => parts {X} \ used evs)" + --{*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"}. *} + +lemma Notes_imp_used [rule_format]: "Notes A X \ set evs --> X \ used evs" +apply (induct_tac evs) +apply (auto split: event.split) +done + +lemma Says_imp_used [rule_format]: "Says A B X \ set evs --> X \ used evs" +apply (induct_tac evs) +apply (auto split: event.split) +done + + +subsection{*Function @{term knows}*} + +(*Simplifying + parts(insert X (knows Spy evs)) = parts{X} \ parts(knows Spy evs). + This version won't loop with the simplifier.*) +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard] + +lemma knows_Spy_Says [simp]: + "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"}*} +lemma knows_Spy_Notes [simp]: + "knows Spy (Notes A X # evs) = + (if A:bad then insert X (knows Spy evs) else knows Spy evs)" +by simp + +lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs" +by simp + +lemma knows_Spy_subset_knows_Spy_Says: + "knows Spy evs \ knows Spy (Says A B X # evs)" +by (simp add: subset_insertI) + +lemma knows_Spy_subset_knows_Spy_Notes: + "knows Spy evs \ knows Spy (Notes A X # evs)" +by force + +lemma knows_Spy_subset_knows_Spy_Gets: + "knows Spy evs \ knows Spy (Gets A X # evs)" +by (simp add: subset_insertI) + +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") +apply (simp_all (no_asm_simp) split add: event.split) +done + +lemma Notes_imp_knows_Spy [rule_format]: + "Notes A X \ set evs --> A: bad --> X \ knows Spy evs" +apply (induct_tac "evs") +apply (simp_all (no_asm_simp) split add: event.split) +done + + +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, THEN revcut_rl, standard] + parts.Body [THEN revcut_rl, standard] + +lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj] + +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*} + +lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)" +by simp + +lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)" +by simp + +lemma knows_Gets: + "A \ Spy --> knows A (Gets A X # evs) = insert X (knows A evs)" +by simp + + +lemma knows_subset_knows_Says: "knows A evs \ knows A (Says A' B X # evs)" +by (simp add: subset_insertI) + +lemma knows_subset_knows_Notes: "knows A evs \ knows A (Notes A' X # evs)" +by (simp add: subset_insertI) + +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*} +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 add: event.split) +apply blast +done + +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 add: event.split) +apply blast +done + +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") +apply (simp_all (no_asm_simp) split add: event.split) +done -use "Event_lemmas.ML" +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" +apply (erule rev_mp) +apply (induct_tac "evs") +apply (simp_all (no_asm_simp) split add: event.split) +apply blast +done + +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" +apply (erule rev_mp) +apply (induct_tac "evs") +apply (simp_all (no_asm_simp) split add: event.split) +apply blast +done + +lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \ used evs" +apply (induct_tac "evs", force) +apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) +done + +lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] + +lemma initState_into_used: "X \ parts (initState B) ==> X \ used evs" +apply (induct_tac "evs") +apply (simp_all add: parts_insert_knows_A split add: event.split, blast) +done + +lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \ used evs" +by simp + +lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \ used evs" +by simp + +lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" +by simp + +lemma used_nil_subset: "used [] \ used evs" +apply simp +apply (blast intro: initState_into_used) +done + +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"} + 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}.*} + +lemmas analz_mono_contra = + knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] + knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] + knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] + +ML +{* +val analz_mono_contra_tac = + let val analz_impI = inst "P" "?Y \ analz (knows Spy ?evs)" impI + in + rtac analz_impI THEN' + REPEAT1 o + (dresolve_tac (thms"analz_mono_contra")) + THEN' mp_tac + end +*} + + +lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" +by (induct e, auto simp: knows_Cons) + +lemma initState_subset_knows: "initState A \ knows A evs" +apply (induct_tac evs, simp) +apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) +done + + +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"; +by (force + dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] + 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 = {* - Method.no_args - (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *} + Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} "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*} + +ML +{* +val knows_Cons = thm "knows_Cons" +val used_Nil = thm "used_Nil" +val used_Cons = thm "used_Cons" + +val Notes_imp_used = thm "Notes_imp_used"; +val Says_imp_used = thm "Says_imp_used"; +val Says_imp_knows_Spy = thm "Says_imp_knows_Spy"; +val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy"; +val knows_Spy_partsEs = thms "knows_Spy_partsEs"; +val spies_partsEs = thms "spies_partsEs"; +val Says_imp_spies = thm "Says_imp_spies"; +val parts_insert_spies = thm "parts_insert_spies"; +val Says_imp_knows = thm "Says_imp_knows"; +val Notes_imp_knows = thm "Notes_imp_knows"; +val Gets_imp_knows_agents = thm "Gets_imp_knows_agents"; +val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState"; +val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState"; +val usedI = thm "usedI"; +val initState_into_used = thm "initState_into_used"; +val used_Says = thm "used_Says"; +val used_Notes = thm "used_Notes"; +val used_Gets = thm "used_Gets"; +val used_nil_subset = thm "used_nil_subset"; +val analz_mono_contra = thms "analz_mono_contra"; +val knows_subset_knows_Cons = thm "knows_subset_knows_Cons"; +val initState_subset_knows = thm "initState_subset_knows"; +val keysFor_parts_insert = thm "keysFor_parts_insert"; + + +val synth_analz_mono = thm "synth_analz_mono"; + +val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says"; +val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes"; +val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets"; + + +val synth_analz_mono_contra_tac = + let val syan_impI = inst "P" "?Y \ synth (analz (knows Spy ?evs))" impI + in + rtac syan_impI THEN' + REPEAT1 o + (dresolve_tac + [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD, + knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD, + knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD]) + THEN' + mp_tac + end; +*} + +method_setup synth_analz_mono_contra = {* + Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *} + "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" +(*>*) + +section{* Event Traces \label{sec:events} *} + +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$. +A trace is simply a list, constructed in reverse +using~@{text "#"}. Other event types include reception of messages (when +we want to make it explicit) and an agent's storing a fact. + +Sometimes the protocol requires an agent to generate a new nonce. The +probability that a 20-byte random number has appeared before is effectively +zero. To formalize this important property, the set @{term "used evs"} +denotes the set of all items mentioned in the trace~@{text evs}. +The function @{text used} has a straightforward +recursive definition. Here is the case for @{text Says} event: +@{thm [display,indent=5] used_Says [no_vars]} + +The function @{text knows} formalizes an agent's knowledge. Mostly we only +care about the spy's knowledge, and @{term "knows Spy evs"} is the set of items +available to the spy in the trace~@{text evs}. Already in the empty trace, +the spy starts with some secrets at his disposal, such as the private keys +of compromised users. After each @{text Says} event, the spy learns the +message that was sent: +@{thm [display,indent=5] knows_Spy_Says [no_vars]} +Combinations of functions express other important +sets of messages derived from~@{text evs}: +\begin{itemize} +\item @{term "analz (knows Spy evs)"} is everything that the spy could +learn by decryption +\item @{term "synth (analz (knows Spy evs))"} is everything that the spy +could generate +\end{itemize} +*} + +(*<*) end +(*>*) \ No newline at end of file diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jul 23 14:30:53 2007 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jul 23 14:31:34 2007 +0200 @@ -5,45 +5,83 @@ Datatypes of agents and messages; Inductive relations "parts", "analz" and "synth" -*) +*)(*<*) -theory Message imports Main -uses ("Message_lemmas.ML") begin +header{*Theory of Agents and Messages for Security Protocols*} + +theory Message imports Main uses "../../antiquote_setup.ML" begin (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) -lemma [simp] : "A Un (B Un A) = B Un A" +lemma [simp] : "A \ (B \ A) = B \ A" by blast +(*>*) + +section{* Agents and Messages *} -types - key = nat +text {* +All protocol specifications refer to a syntactic theory of messages. +Datatype +@{text agent} introduces the constant @{text Server} (a trusted central +machine, needed for some protocols), an infinite population of +friendly agents, and the~@{text Spy}: +*} + +datatype agent = Server | Friend nat | Spy -consts - invKey :: "key=>key" +text {* +Keys are just natural numbers. Function @{text invKey} maps a public key to +the matching private key, and vice versa: +*} -axioms - invKey [simp] : "invKey (invKey K) = K" +types key = nat +consts invKey :: "key=>key" +(*<*) +consts all_symmetric :: bool --{*true if all keys are symmetric*} - (*The inverse of a symmetric key is itself; - that of a public key is the private key and vice versa*) +specification (invKey) + invKey [simp]: "invKey (invKey K) = K" + invKey_symmetric: "all_symmetric --> invKey = id" + 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*} constdefs symKeys :: "key set" "symKeys == {K. invKey K = K}" +(*>*) -datatype (*We allow any number of friendly agents*) - agent = Server | Friend nat | Spy +text {* +Datatype +@{text msg} introduces the message forms, which include agent names, nonces, +keys, compound messages, and encryptions. +*} 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 + | Nonce nat + | Key key + | MPair msg msg + | Crypt key msg + +text {* +\noindent +The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ +abbreviates +$\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. +Since datatype constructors are injective, we have the theorem +@{thm [display,indent=0] msg.inject(5) [THEN iffD1, of K X K' X']} +A ciphertext can be decrypted using only one key and +can yield only one plaintext. In the real world, decryption with the +wrong key succeeds but yields garbage. Our model of encryption is +realistic if encryption adds some redundancy to the plaintext, such as a +checksum, so that garbage can be detected. +*} -(*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{|_,/ _|})") @@ -56,18 +94,15 @@ constdefs - (*Message Y, paired with a MAC computed with the help of X*) - HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) - "Hash[X] Y == {| Hash{|X,Y|}, Y|}" - - (*Keys useful to decrypt elements of a message set*) keysFor :: "msg set => key set" + --{*Keys useful to decrypt elements of a message set*} "keysFor H == invKey ` {K. \X. Crypt K X \ H}" -(** Inductive definition of all "parts" of a message. **) + +subsubsection{*Inductive Definition of All Parts" of a Message*} inductive_set - parts :: "msg set => msg set" + parts :: "msg set => msg set" for H :: "msg set" where Inj [intro]: "X \ H ==> X \ parts H" @@ -76,75 +111,825 @@ | Body: "Crypt K X \ parts H ==> X \ parts H" -(*Monotonicity*) -lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" +text{*Monotonicity*} +lemma parts_mono: "G \ H ==> parts(G) \ parts(H)" apply auto apply (erule parts.induct) -apply (auto dest: Fst Snd Body) +apply (blast dest: parts.Fst parts.Snd parts.Body)+ +done + + +text{*Equations hold because constructors are injective.*} +lemma Friend_image_eq [simp]: "(Friend x \ Friend`A) = (x:A)" +by auto + +lemma Key_image_eq [simp]: "(Key x \ Key`A) = (x\A)" +by auto + +lemma Nonce_Key_image_eq [simp]: "(Nonce x \ Key`A)" +by auto + + +subsubsection{*Inverse of keys *} + +lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')" +apply safe +apply (drule_tac f = invKey in arg_cong, simp) +done + + +subsection{*keysFor operator*} + +lemma keysFor_empty [simp]: "keysFor {} = {}" +by (unfold keysFor_def, blast) + +lemma keysFor_Un [simp]: "keysFor (H \ H') = keysFor H \ keysFor H'" +by (unfold keysFor_def, blast) + +lemma keysFor_UN [simp]: "keysFor (\i\A. H i) = (\i\A. keysFor (H i))" +by (unfold keysFor_def, blast) + +text{*Monotonicity*} +lemma keysFor_mono: "G \ H ==> keysFor(G) \ keysFor(H)" +by (unfold keysFor_def, blast) + +lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H" +by (unfold keysFor_def, auto) + +lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H" +by (unfold keysFor_def, auto) + +lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H" +by (unfold keysFor_def, auto) + +lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H" +by (unfold keysFor_def, auto) + +lemma keysFor_insert_Crypt [simp]: + "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" +by (unfold keysFor_def, auto) + +lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}" +by (unfold keysFor_def, auto) + +lemma Crypt_imp_invKey_keysFor: "Crypt K X \ H ==> invKey K \ keysFor H" +by (unfold keysFor_def, blast) + + +subsection{*Inductive relation "parts"*} + +lemma MPair_parts: + "[| {|X,Y|} \ parts H; + [| X \ parts H; Y \ parts H |] ==> P |] ==> P" +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 + 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.*} + +lemma parts_increasing: "H \ parts(H)" +by blast + +lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard] + +lemma parts_empty [simp]: "parts{} = {}" +apply safe +apply (erule parts.induct, blast+) +done + +lemma parts_emptyE [elim!]: "X\ parts{} ==> P" +by simp + +text{*WARNING: loops if H = {Y}, therefore must not be repeated!*} +lemma parts_singleton: "X\ parts H ==> \Y\H. X\ parts {Y}" +by (erule parts.induct, blast+) + + +subsubsection{*Unions *} + +lemma parts_Un_subset1: "parts(G) \ parts(H) \ parts(G \ H)" +by (intro Un_least parts_mono Un_upper1 Un_upper2) + +lemma parts_Un_subset2: "parts(G \ H) \ parts(G) \ parts(H)" +apply (rule subsetI) +apply (erule parts.induct, blast+) +done + +lemma parts_Un [simp]: "parts(G \ H) = parts(G) \ parts(H)" +by (intro equalityI parts_Un_subset1 parts_Un_subset2) + +lemma parts_insert: "parts (insert X H) = parts {X} \ parts H" +apply (subst insert_is_Un [of _ H]) +apply (simp only: parts_Un) +done + +text{*TWO inserts to avoid looping. This rewrite is better than nothing. + Not suitable for Addsimps: its behaviour can be strange.*} +lemma parts_insert2: + "parts (insert X (insert Y H)) = parts {X} \ parts {Y} \ parts H" +apply (simp add: Un_assoc) +apply (simp add: parts_insert [symmetric]) +done + +lemma parts_UN_subset1: "(\x\A. parts(H x)) \ parts(\x\A. H x)" +by (intro UN_least parts_mono UN_upper) + +lemma parts_UN_subset2: "parts(\x\A. H x) \ (\x\A. parts(H x))" +apply (rule subsetI) +apply (erule parts.induct, blast+) +done + +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{*This allows @{text 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 *} + +lemma parts_partsD [dest!]: "X\ parts (parts H) ==> X\ parts H" +by (erule parts.induct, blast+) + +lemma parts_idem [simp]: "parts (parts H) = parts H" +by blast + +lemma parts_subset_iff [simp]: "(parts G \ parts H) = (G \ parts H)" +apply (rule iffI) +apply (iprover intro: subset_trans parts_increasing) +apply (frule parts_mono, simp) +done + +lemma parts_trans: "[| X\ parts G; G \ parts H |] ==> X\ parts H" +by (drule parts_mono, blast) + +text{*Cut*} +lemma parts_cut: + "[| Y\ parts (insert X G); X\ parts H |] ==> Y\ parts (G \ H)" +by (blast intro: parts_trans) + + +lemma parts_cut_eq [simp]: "X\ parts H ==> parts (insert X H) = parts H" +by (force dest!: parts_cut intro: parts_insertI) + + +subsubsection{*Rewrite rules for pulling out atomic messages *} + +lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] + + +lemma parts_insert_Agent [simp]: + "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) +done + +lemma parts_insert_Nonce [simp]: + "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) +done + +lemma parts_insert_Key [simp]: + "parts (insert (Key K) H) = insert (Key K) (parts H)" +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) +done + +lemma parts_insert_Crypt [simp]: + "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))" +apply (rule equalityI) +apply (rule subsetI) +apply (erule parts.induct, auto) +apply (blast intro: parts.Body) +done + +lemma parts_insert_MPair [simp]: + "parts (insert {|X,Y|} H) = + insert {|X,Y|} (parts (insert X (insert Y H)))" +apply (rule equalityI) +apply (rule subsetI) +apply (erule parts.induct, auto) +apply (blast intro: parts.Fst parts.Snd)+ +done + +lemma parts_image_Key [simp]: "parts (Key`N) = Key`N" +apply auto +apply (erule parts.induct, auto) done -(** 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. **) +text{*In any message, there is an upper bound N on its greatest nonce.*} +lemma msg_Nonce_supply: "\N. \n. N\n --> Nonce n \ parts {msg}" +apply (induct_tac "msg") +apply (simp_all (no_asm_simp) add: exI parts_insert2) + txt{*MPair case: blast works out the necessary sum itself!*} + prefer 2 apply auto apply (blast elim!: add_leE) +txt{*Nonce case*} +apply (rule_tac x = "N + Suc nat" in exI, auto) +done +(*>*) + +section{* Modelling the Adversary *} + +text {* +The spy is part of the system and must be built into the model. He is +a malicious user who does not have to follow the protocol. He +watches the network and uses any keys he knows to decrypt messages. +Thus he accumulates additional keys and nonces. These he can use to +compose new messages, which he may send to anybody. + +Two functions enable us to formalize this behaviour: @{text analz} and +@{text synth}. Each function maps a sets of messages to another set of +messages. The set @{text "analz H"} formalizes what the adversary can learn +from the set of messages~$H$. The closure properties of this set are +defined inductively. +*} inductive_set - analz :: "msg set => msg set" + analz :: "msg set \ msg set" for H :: "msg set" where - Inj [intro,simp] : "X \ H ==> X \ analz H" - | Fst: "{|X,Y|} \ analz H ==> X \ analz H" - | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + Inj [intro,simp] : "X \ H \ X \ analz H" + | Fst: "\X,Y\ \ analz H \ X \ analz H" + | Snd: "\X,Y\ \ analz H \ Y \ analz H" | Decrypt [dest]: - "[|Crypt K X \ analz H; Key(invKey K) \ analz H|] ==> X \ analz H" + "\Crypt K X \ analz H; Key(invKey K) \ analz H\ + \ X \ analz H" +(*<*) +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*} +lemma MPair_analz [elim!]: + "[| {|X,Y|} \ analz H; + [| X \ analz H; Y \ analz H |] ==> P + |] ==> P" +by (blast dest: analz.Fst analz.Snd) + +lemma analz_increasing: "H \ analz(H)" +by blast + +lemma analz_subset_parts: "analz H \ parts H" +apply (rule subsetI) +apply (erule analz.induct, blast+) +done + +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] + +lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard] -(*Monotonicity; Lemma 1 of Lowe's paper*) -lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" +lemma parts_analz [simp]: "parts (analz H) = parts H" +apply (rule equalityI) +apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp) +apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD]) +done + +lemma analz_parts [simp]: "analz (parts H) = parts H" apply auto -apply (erule analz.induct) -apply (auto dest: Fst Snd) +apply (erule analz.induct, auto) +done + +lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard] + +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*} +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 *} + +lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] + +lemma analz_insert_Agent [simp]: + "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) +done + +lemma analz_insert_Nonce [simp]: + "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) +done + +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)" +apply (unfold keysFor_def) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) +done + +lemma analz_insert_MPair [simp]: + "analz (insert {|X,Y|} H) = + insert {|X,Y|} (analz (insert X (insert Y H)))" +apply (rule equalityI) +apply (rule subsetI) +apply (erule analz.induct, auto) +apply (erule analz.induct) +apply (blast intro: analz.Fst analz.Snd)+ +done + +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)" +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) + done -(** 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. **) +lemma lemma1: "Key (invKey K) \ analz H ==> + analz (insert (Crypt K X) H) \ + insert (Crypt K X) (analz (insert X H))" +apply (rule subsetI) +apply (erule_tac x = x in analz.induct, auto) +done + +lemma lemma2: "Key (invKey K) \ analz H ==> + insert (Crypt K X) (analz (insert X H)) \ + analz (insert (Crypt K X) H)" +apply auto +apply (erule_tac x = x in analz.induct, auto) +apply (blast intro: analz_insertI analz.Decrypt) +done + +lemma analz_insert_Decrypt: + "Key (invKey K) \ analz H ==> + analz (insert (Crypt K X) H) = + 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 "split_if"}; apparently +@{text "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) + then insert (Crypt K X) (analz (insert X H)) + else insert (Crypt K X) (analz H))" +by (simp add: analz_insert_Crypt analz_insert_Decrypt) + + +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))" +apply (rule subsetI) +apply (erule analz.induct, auto) +done + + +lemma analz_image_Key [simp]: "analz (Key`N) = Key`N" +apply auto +apply (erule analz.induct, auto) +done + + +subsubsection{*Idempotence and transitivity *} + +lemma analz_analzD [dest!]: "X\ analz (analz H) ==> X\ analz H" +by (erule analz.induct, blast+) + +lemma analz_idem [simp]: "analz (analz H) = analz H" +by blast + +lemma analz_subset_iff [simp]: "(analz G \ analz H) = (G \ analz H)" +apply (rule iffI) +apply (iprover intro: subset_trans analz_increasing) +apply (frule analz_mono, simp) +done + +lemma analz_trans: "[| X\ analz G; G \ analz H |] ==> X\ analz H" +by (drule analz_mono, blast) + +text{*Cut; Lemma 2 of Lowe*} +lemma analz_cut: "[| Y\ analz (insert X H); X\ analz H |] ==> Y\ analz H" +by (erule analz_trans, blast) + +(*Cut can be proved easily by induction on + "Y: analz (insert X H) ==> X: analz H --> Y: analz H" +*) + +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. *} +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" *} + +lemma analz_subset_cong: + "[| analz G \ analz G'; analz H \ analz H' |] + ==> analz (G \ H) \ analz (G' \ H')" +apply simp +apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) +done + +lemma analz_cong: + "[| analz G = analz G'; analz H = analz H' |] + ==> analz (G \ H) = analz (G' \ H')" +by (intro equalityI analz_subset_cong, simp_all) + +lemma analz_insert_cong: + "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*} +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...*} +lemma analz_UN_analz_lemma: + "X\ analz (\i\A. analz (H i)) ==> X\ analz (\i\A. H i)" +apply (erule analz.induct) +apply (blast intro: analz_mono [THEN [2] rev_subsetD])+ +done + +lemma analz_UN_analz [simp]: "analz (\i\A. analz (H i)) = analz (\i\A. H i)" +by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD]) +(*>*) +text {* +Note the @{text Decrypt} rule: the spy can decrypt a +message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. +Properties proved by rule induction include the following: +@{named_thms [display,indent=0] analz_mono [no_vars] (analz_mono) analz_idem [no_vars] (analz_idem)} + +The set of fake messages that an intruder could invent +starting from~@{text H} is @{text "synth(analz H)"}, where @{text "synth H"} +formalizes what the adversary can build from the set of messages~$H$. +*} inductive_set - synth :: "msg set => msg set" + synth :: "msg set \ msg set" for H :: "msg set" where - Inj [intro]: "X \ H ==> X \ synth H" - | Agent [intro]: "Agent agt \ synth H" - | Number [intro]: "Number n \ synth H" - | Hash [intro]: "X \ synth H ==> Hash X \ synth H" - | 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" + Inj [intro]: "X \ H \ X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | 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" +(*<*) +lemma synth_mono: "G\H ==> synth(G) \ synth(H)" + by (auto, erule synth.induct, auto) -(*Monotonicity*) -lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" -apply auto -apply (erule synth.induct) -apply (auto dest: Fst Snd Body) -done - -(*NO Agent_synth, as any Agent name can be synthesized. Ditto for 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" inductive_cases MPair_synth [elim!]: "{|X,Y|} \ synth H" inductive_cases Crypt_synth [elim!]: "Crypt K X \ synth H" -use "Message_lemmas.ML" +lemma analz_synth_Un [simp]: "analz (synth G \ H) = analz (G \ H) \ synth G" +apply (rule equalityI) +apply (rule subsetI) +apply (erule analz.induct) +prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD]) +apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+ +done + +lemma analz_synth [simp]: "analz (synth H) = analz H \ synth H" +apply (cut_tac H = "{}" in analz_synth_Un) +apply (simp (no_asm_use)) +done +(*>*) +text {* +The set includes all agent names. Nonces and keys are assumed to be +unguessable, so none are included beyond those already in~$H$. Two +elements of @{term "synth H"} can be combined, and an element can be encrypted +using a key present in~$H$. + +Like @{text analz}, this set operator is monotone and idempotent. It also +satisfies an interesting equation involving @{text analz}: +@{named_thms [display,indent=0] analz_synth [no_vars] (analz_synth)} +Rule inversion plays a major role in reasoning about @{text synth}, through +declarations such as this one: +*} + +inductive_cases Nonce_synth [elim!]: "Nonce n \ synth H" + +text {* +\noindent +The resulting elimination rule replaces every assumption of the form +@{term "Nonce n \ synth H"} by @{term "Nonce n \ H"}, +expressing that a nonce cannot be guessed. + +A third operator, @{text parts}, is useful for stating correctness +properties. The set +@{term "parts H"} consists of the components of elements of~$H$. This set +includes~@{text H} and is closed under the projections from a compound +message to its immediate parts. +Its definition resembles that of @{text analz} except in the rule +corresponding to the constructor @{text Crypt}: +@{thm [display,indent=5] parts.Body [no_vars]} +The body of an encrypted message is always regarded as part of it. We can +use @{text parts} to express general well-formedness properties of a protocol, +for example, that an uncompromised agent's private key will never be +included as a component of any message. +*} +(*<*) +lemma synth_increasing: "H \ synth(H)" +by blast + +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.*} +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 (blast intro: synth_mono [THEN [2] rev_subsetD]) + +subsubsection{*Idempotence and transitivity *} + +lemma synth_synthD [dest!]: "X\ synth (synth H) ==> X\ synth H" +by (erule synth.induct, blast+) + +lemma synth_idem: "synth (synth H) = synth H" +by blast + +lemma synth_subset_iff [simp]: "(synth G \ synth H) = (G \ synth H)" +apply (rule iffI) +apply (iprover intro: subset_trans synth_increasing) +apply (frule synth_mono, simp add: synth_idem) +done + +lemma synth_trans: "[| X\ synth G; G \ synth H |] ==> X\ synth H" +by (drule synth_mono, blast) + +text{*Cut; Lemma 2 of Lowe*} +lemma synth_cut: "[| Y\ synth (insert X H); X\ synth H |] ==> Y\ synth H" +by (erule synth_trans, blast) + +lemma Agent_synth [simp]: "Agent A \ synth H" +by blast + +lemma Nonce_synth_eq [simp]: "(Nonce N \ synth H) = (Nonce N \ H)" +by blast + +lemma Key_synth_eq [simp]: "(Key K \ synth H) = (Key K \ H)" +by blast + +lemma Crypt_synth_eq [simp]: + "Key K \ H ==> (Crypt K X \ synth H) = (Crypt K X \ H)" +by blast + + +lemma keysFor_synth [simp]: + "keysFor (synth H) = keysFor H \ invKey`{K. Key K \ H}" +by (unfold keysFor_def, blast) + + +subsubsection{*Combinations of parts, analz and synth *} + +lemma parts_synth [simp]: "parts (synth H) = parts H \ synth H" +apply (rule equalityI) +apply (rule subsetI) +apply (erule parts.induct) +apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] + parts.Fst parts.Snd parts.Body)+ +done + +lemma analz_analz_Un [simp]: "analz (analz G \ H) = analz (G \ H)" +apply (intro equalityI analz_subset_cong)+ +apply simp_all +done + + +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) + +text{*More specifically for Fake. Very occasionally we could do with a version + of the form @{term"parts{X} \ synth (analz H) \ parts H"} *} +lemma Fake_parts_insert: + "X \ synth (analz H) ==> + parts (insert X H) \ synth (analz H) \ parts H" +apply (drule parts_insert_subset_Un) +apply (simp (no_asm_use)) +apply blast +done lemma Fake_parts_insert_in_Un: "[|Z \ parts (insert X H); X: synth (analz H)|] ==> Z \ synth (analz H) \ parts H"; by (blast dest: Fake_parts_insert [THEN subsetD, dest]) +text{*@{term H} is sometimes @{term"Key ` KK \ spies evs"}, so can't put + @{term "G=H"}.*} +lemma Fake_analz_insert: + "X\ synth (analz G) ==> + analz (insert X H) \ synth (analz G) \ analz (G \ H)" +apply (rule subsetI) +apply (subgoal_tac "x \ analz (synth (analz G) \ H) ") +prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD]) +apply (simp (no_asm_use)) +apply blast +done + +lemma analz_conj_parts [simp]: + "(X \ analz H & X \ parts H) = (X \ analz H)" +by (blast intro: analz_subset_parts [THEN subsetD]) + +lemma analz_disj_parts [simp]: + "(X \ analz H | X \ parts H) = (X \ parts H)" +by (blast intro: analz_subset_parts [THEN subsetD]) + +text{*Without this equation, other rules for synth and analz would yield + redundant cases*} +lemma MPair_synth_analz [iff]: + "({|X,Y|} \ synth (analz H)) = + (X \ synth (analz H) & Y \ synth (analz H))" +by blast + +lemma Crypt_synth_analz: + "[| Key K \ analz H; Key (invKey K) \ analz H |] + ==> (Crypt K X \ synth (analz H)) = (X \ synth (analz H))" +by blast + + +text{*We do NOT want Crypt... messages broken up in protocols!!*} +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*} +ML +{* +fun insComm x y = inst "x" x (inst "y" y insert_commute); + +bind_thms ("pushKeys", + map (insComm "Key ?K") + ["Agent ?C", "Nonce ?N", "Number ?N", + "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); + +bind_thms ("pushCrypts", + map (insComm "Crypt ?X ?K") + ["Agent ?C", "Nonce ?N", "Number ?N", + "Hash ?X'", "MPair ?X' ?Y"]); +*} + +text{*Cannot be added with @{text "[simp]"} -- messages should not always be + re-ordered. *} +lemmas pushes = pushKeys pushCrypts + + +subsection{*Tactics useful for many protocol proofs*} +ML +{* +val invKey = thm "invKey" +val keysFor_def = thm "keysFor_def" +val symKeys_def = thm "symKeys_def" +val parts_mono = thm "parts_mono"; +val analz_mono = thm "analz_mono"; +val synth_mono = thm "synth_mono"; +val analz_increasing = thm "analz_increasing"; + +val analz_insertI = thm "analz_insertI"; +val analz_subset_parts = thm "analz_subset_parts"; +val Fake_parts_insert = thm "Fake_parts_insert"; +val Fake_analz_insert = thm "Fake_analz_insert"; +val pushes = thms "pushes"; + + +(*Prove base case (subgoal i) and simplify others. A typical base case + concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting + alone.*) +fun prove_simple_subgoals_tac i = + force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN + ALLGOALS Asm_simp_tac + +(*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. + Abstraction over i is ESSENTIAL: it delays the dereferencing of claset + DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) + +(*Apply rules to break down assumptions of the form + Y \ parts(insert X H) and Y \ analz(insert X H) +*) +val Fake_insert_tac = + dresolve_tac [impOfSubs Fake_analz_insert, + impOfSubs Fake_parts_insert] THEN' + eresolve_tac [asm_rl, thm"synth.Inj"]; + +fun Fake_insert_simp_tac ss i = + REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; + +fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL + (Fake_insert_simp_tac ss 1 + THEN + IF_UNSOLVED (Blast.depth_tac + (cs addIs [analz_insertI, + impOfSubs analz_subset_parts]) 4 1)) + +(*The explicit claset and simpset arguments help it work with Isar*) +fun gen_spy_analz_tac (cs,ss) i = + DETERM + (SELECT_GOAL + (EVERY + [ (*push in occurrences of X...*) + (REPEAT o CHANGED) + (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), + (*...allowing further simplifications*) + simp_tac ss 1, + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), + DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) + +fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i +*} + +text{*By default only @{text o_apply} is built-in. But in the presence of +eta-expansion this means that some terms displayed as @{term "f o g"} will be +rewritten, and others will not!*} +declare o_def [simp] + + +lemma Crypt_notin_image_Key [simp]: "Crypt K X \ Key ` A" +by auto + +lemma synth_analz_mono: "G\H ==> synth (analz(G)) \ synth (analz(H))" +by (iprover intro: synth_mono analz_mono) + +lemma Fake_analz_eq [simp]: + "X \ synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)" +apply (drule Fake_analz_insert[of _ _ "H"]) +apply (simp add: synth_increasing[THEN Un_absorb2]) +apply (drule synth_mono) +apply (simp add: synth_idem) +apply (rule equalityI) +apply (simp add: ); +apply (rule synth_analz_mono, blast) +done + +text{*Two generalizations of @{text 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]) + +lemma synth_analz_insert_eq [rule_format]: + "X \ synth (analz H) + ==> ALL G. H \ G --> (Key K \ analz (insert X G)) = (Key K \ analz G)"; +apply (erule synth.induct) +apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) +done + +lemma Fake_parts_sing: + "X \ synth (analz H) ==> parts{X} \ synth (analz H) \ parts H"; +apply (rule subset_trans) + apply (erule_tac [2] Fake_parts_insert) +apply (rule parts_mono, blast) +done + +lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] + method_setup spy_analz = {* - Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} + Method.ctxt_args (fn ctxt => + Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} "for proving the Fake case when analz is involved" +method_setup atomic_spy_analz = {* + Method.ctxt_args (fn ctxt => + Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + "for debugging spy_analz" + +method_setup Fake_insert_simp = {* + Method.ctxt_args (fn ctxt => + Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} + "for debugging spy_analz" + + end +(*>*) \ No newline at end of file diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/NS_Public.thy --- a/doc-src/TutorialI/Protocol/NS_Public.thy Mon Jul 23 14:30:53 2007 +0200 +++ b/doc-src/TutorialI/Protocol/NS_Public.thy Mon Jul 23 14:31:34 2007 +0200 @@ -5,40 +5,92 @@ Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. Version incorporating Lowe's fix (inclusion of B's identity in round 2). -*) +*)(*<*) +theory NS_Public imports Public begin(*>*) -theory NS_Public imports Public begin +section{* Modelling the Protocol \label{sec:modelling} *} -inductive_set - ns_public :: "event list set" +text_raw {* +\begin{figure} +\begin{isabelle} +*} + +inductive_set ns_public :: "event list set" where - (*Initial trace is empty*) + Nil: "[] \ ns_public" - (*The spy MAY say anything he CAN say. We do not expect him to - invent new nonces here, but he can also use NS1. Common to - all similar protocols.*) - | Fake: "\evs \ ns_public; X \ synth (analz (knows Spy evs))\ - \ Says Spy B X # evs \ ns_public" - (*Alice initiates a protocol run, sending a nonce to Bob*) + | Fake: "\evsf \ ns_public; X \ synth (analz (knows Spy evsf))\ + \ Says Spy B X # evsf \ ns_public" + + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubK B) \Nonce NA, Agent A\) # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) # evs2 \ ns_public" - (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs3; Says B' A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs3\ \ Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \ ns_public" +text_raw {* +\end{isabelle} +\caption{An Inductive Protocol Definition}\label{fig:ns_public} +\end{figure} +*} + +text {* +Let us formalize the Needham-Schroeder public-key protocol, as corrected by +Lowe: +\begin{alignat*% +}{2} + &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ + &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ + &3.&\quad A\to B &: \comp{Nb}\sb{Kb} +\end{alignat*% +} + +Each protocol step is specified by a rule of an inductive definition. An +event trace has type @{text "event list"}, so we declare the constant +@{text ns_public} to be a set of such traces. + +Figure~\ref{fig:ns_public} presents the inductive definition. The +@{text Nil} rule introduces the empty trace. The @{text Fake} rule models the +adversary's sending a message built from components taken from past +traffic, expressed using the functions @{text synth} and +@{text analz}. +The next three rules model how honest agents would perform the three +protocol steps. + +Here is a detailed explanation of rule @{text NS2}. +A trace containing an event of the form +@{term [display,indent=5] "Says A' B (Crypt (pubK B) \Nonce NA, Agent A\)"} +may be extended by an event of the form +@{term [display,indent=5] "Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\)"} +where @{text NB} is a fresh nonce: @{term "Nonce NB \ used evs2"}. +Writing the sender as @{text A'} indicates that @{text B} does not +know who sent the message. Calling the trace variable @{text evs2} rather +than simply @{text evs} helps us know where we are in a proof after many +case-splits: every subgoal mentioning @{text evs2} involves message~2 of the +protocol. + +Benefits of this approach are simplicity and clarity. The semantic model +is set theory, proofs are by induction and the translation from the informal +notation to the inductive rules is straightforward. +*} + +section{* Proving Elementary Properties \label{sec:regularity} *} + +(*<*) declare knows_Spy_partsEs [elim] declare analz_subset_parts [THEN subsetD, dest] declare Fake_parts_insert [THEN subsetD, dest] @@ -58,43 +110,98 @@ sends messages containing X! **) (*Spy never sees another agent's private key! (unless it's bad at start)*) +(*>*) + +text {* +Secrecy properties can be hard to prove. The conclusion of a typical +secrecy theorem is +@{term "X \ analz (knows Spy evs)"}. The difficulty arises from +having to reason about @{text analz}, or less formally, showing that the spy +can never learn~@{text X}. Much easier is to prove that @{text X} can never +occur at all. Such \emph{regularity} properties are typically expressed +using @{text parts} rather than @{text analz}. + +The following lemma states that @{text A}'s private key is potentially +known to the spy if and only if @{text A} belongs to the set @{text bad} of +compromised agents. The statement uses @{text parts}: the very presence of +@{text A}'s private key in a message, whether protected by encryption or +not, is enough to confirm that @{text A} is compromised. The proof, like +nearly all protocol proofs, is by induction over traces. +*} + lemma Spy_see_priK [simp]: - "evs \ ns_public \ (Key (priK A) \ parts (knows Spy evs)) = (A \ bad)" -by (erule ns_public.induct, auto) + "evs \ ns_public + \ (Key (priK A) \ parts (knows Spy evs)) = (A \ bad)" +apply (erule ns_public.induct, simp_all) +txt {* +The induction yields five subgoals, one for each rule in the definition of +@{text ns_public}. The idea is to prove that the protocol property holds initially +(rule @{text Nil}), is preserved by each of the legitimate protocol steps (rules +@{text NS1}--@{text 3}), and even is preserved in the face of anything the +spy can do (rule @{text Fake}). +The proof is trivial. No legitimate protocol rule sends any keys +at all, so only @{text Fake} is relevant. Indeed, simplification leaves +only the @{text Fake} case, as indicated by the variable name @{text evsf}: +@{subgoals[display,indent=0,margin=65]} +*} +by blast +(*<*) lemma Spy_analz_priK [simp]: "evs \ ns_public \ (Key (priK A) \ analz (knows Spy evs)) = (A \ bad)" by auto - +(*>*) -(*** Authenticity properties obtained from NS2 ***) - +text {* +The @{text Fake} case is proved automatically. If +@{term "priK A"} is in the extended trace then either (1) it was already in the +original trace or (2) it was +generated by the spy, who must have known this key already. +Either way, the induction hypothesis applies. -(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce - is secret. (Honest users generate fresh nonces.)*) +\emph{Unicity} lemmas are regularity lemmas stating that specified items +can occur only once in a trace. The following lemma states that a nonce +cannot be used both as $Na$ and as $Nb$ unless +it is known to the spy. Intuitively, it holds because honest agents +always choose fresh values as nonces; only the spy might reuse a value, +and he doesn't know this particular value. The proof script is short: +induction, simplification, @{text blast}. The first line uses the rule +@{text rev_mp} to prepare the induction by moving two assumptions into the +induction formula. +*} + lemma no_nonce_NS1_NS2: - "\Crypt (pubK C) \NA', Nonce NA, Agent D\ \ parts (knows Spy evs); - Crypt (pubK B) \Nonce NA, Agent A\ \ parts (knows Spy evs); - evs \ ns_public\ - \ Nonce NA \ analz (knows Spy evs)" + "\Crypt (pubK C) \NA', Nonce NA, Agent D\ \ parts (knows Spy evs); + Crypt (pubK B) \Nonce NA, Agent A\ \ parts (knows Spy evs); + evs \ ns_public\ + \ Nonce NA \ analz (knows Spy evs)" apply (erule rev_mp, erule rev_mp) apply (erule ns_public.induct, simp_all) apply (blast intro: analz_insertI)+ done -(*Unicity for NS1: nonce NA identifies agents A and B*) +text {* +The following unicity lemma states that, if \isa{NA} is secret, then its +appearance in any instance of message~1 determines the other components. +The proof is similar to the previous one. +*} + lemma unique_NA: "\Crypt(pubK B) \Nonce NA, Agent A \ \ parts(knows Spy evs); Crypt(pubK B') \Nonce NA, Agent A'\ \ parts(knows Spy evs); Nonce NA \ analz (knows Spy evs); evs \ ns_public\ \ A=A' \ B=B'" +(*<*) apply (erule rev_mp, erule rev_mp, erule rev_mp) apply (erule ns_public.induct, simp_all) (*Fake, NS1*) apply (blast intro: analz_insertI)+ done +(*>*) +section{* Proving Secrecy Theorems \label{sec:secrecy} *} +(*<*) (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure The major premise "Says A B ..." makes it a dest-rule, so we use (erule rev_mp) rather than rule_format. *) @@ -158,40 +265,97 @@ (*Fake, NS2*) apply (blast intro: analz_insertI)+ done - - +(*>*) -text{* -@{thm[display] analz_Crypt_if[no_vars]} -\rulename{analz_Crypt_if} +text {* +The secrecy theorems for Bob (the second participant) are especially +important because they fail for the original protocol. The following +theorem states that if Bob sends message~2 to Alice, and both agents are +uncompromised, then Bob's nonce will never reach the spy. +*} + +theorem Spy_not_see_NB [dest]: + "\Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ + \ Nonce NB \ analz (knows Spy evs)" +txt {* +To prove it, we must formulate the induction properly (one of the +assumptions mentions~@{text evs}), apply induction, and simplify: *} -(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) -theorem Spy_not_see_NB [dest]: - "\Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ - \ Nonce NB \ analz (knows Spy evs)" -apply (erule rev_mp) -apply (erule ns_public.induct, simp_all) +apply (erule rev_mp, erule ns_public.induct, simp_all) +(*<*) apply spy_analz -apply (blast intro: no_nonce_NS1_NS2)+ -done +defer +apply (blast intro: no_nonce_NS1_NS2) +apply (blast intro: no_nonce_NS1_NS2) +(*>*) + +txt {* +The proof states are too complicated to present in full. +Let's examine the simplest subgoal, that for message~1. The following +event has just occurred: +\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \] +The variables above have been primed because this step +belongs to a different run from that referred to in the theorem +statement --- the theorem +refers to a past instance of message~2, while this subgoal +concerns message~1 being sent just now. +In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$ +we have @{text Ba} and~@{text NAa}: +@{subgoals[display,indent=0]} +The simplifier has used a +default simplification rule that does a case +analysis for each encrypted message on whether or not the decryption key +is compromised. +@{named_thms [display,indent=0,margin=50] analz_Crypt_if [no_vars] (analz_Crypt_if)} +The simplifier has also used @{text Spy_see_priK}, proved in +{\S}\ref{sec:regularity}) above, to yield @{term "Ba \ bad"}. +Recall that this subgoal concerns the case +where the last message to be sent was +\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \] +This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised, +allowing the spy to decrypt the message. The Isabelle subgoal says +precisely this, if we allow for its choice of variable names. +Proving @{term "NB \ NAa"} is easy: @{text NB} was +sent earlier, while @{text NAa} is fresh; formally, we have +the assumption @{term "Nonce NAa \ used evs1"}. -(*Authentication for B: if he receives message 3 and has used NB - in message 2, then A has sent message 3.*) +Note that our reasoning concerned @{text B}'s participation in another +run. Agents may engage in several runs concurrently, and some attacks work +by interleaving the messages of two runs. With model checking, this +possibility can cause a state-space explosion, and for us it +certainly complicates proofs. The biggest subgoal concerns message~2. It +splits into several cases, such as whether or not the message just sent is +the very message mentioned in the theorem statement. +Some of the cases are proved by unicity, others by +the induction hypothesis. For all those complications, the proofs are +automatic by @{text blast} with the theorem @{text no_nonce_NS1_NS2}. + +The remaining theorems about the protocol are not hard to prove. The +following one asserts a form of \emph{authenticity}: if +@{text B} has sent an instance of message~2 to~@{text A} and has received the +expected reply, then that reply really originated with~@{text A}. The +proof is a simple induction. +*} + +(*<*) +by (blast intro: no_nonce_NS1_NS2) + lemma B_trusts_NS3_lemma [rule_format]: "\A \ bad; B \ bad; evs \ ns_public\ \ Crypt (pubK B) (Nonce NB) \ parts (knows Spy evs) \ Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs \ Says A B (Crypt (pubK B) (Nonce NB)) \ set evs" by (erule ns_public.induct, auto) - +(*>*) theorem B_trusts_NS3: - "\Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; - Says A' B (Crypt (pubK B) (Nonce NB)) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ - \ Says A B (Crypt (pubK B) (Nonce NB)) \ set evs" + "\Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; + Says A' B (Crypt (pubK B) (Nonce NB)) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ + \ Says A B (Crypt (pubK B) (Nonce NB)) \ set evs" +(*<*) by (blast intro: B_trusts_NS3_lemma) (*** Overall guarantee for B ***) @@ -199,11 +363,41 @@ (*If NS3 has been sent and the nonce NB agrees with the nonce B joined with NA, then A initiated the run using NA.*) -theorem B_trusts_protocol: +theorem B_trusts_protocol [rule_format]: "\A \ bad; B \ bad; evs \ ns_public\ \ Crypt (pubK B) (Nonce NB) \ parts (knows Spy evs) \ Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs \ Says A B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs" by (erule ns_public.induct, auto) +(*>*) -end +text {* +From similar assumptions, we can prove that @{text A} started the protocol +run by sending an instance of message~1 involving the nonce~@{text NA}\@. +For this theorem, the conclusion is +@{thm_style [display] concl B_trusts_protocol [no_vars]} +Analogous theorems can be proved for~@{text A}, stating that nonce~@{text NA} +remains secret and that message~2 really originates with~@{text B}. Even the +flawed protocol establishes these properties for~@{text A}; +the flaw only harms the second participant. + +\medskip + +Detailed information on this protocol verification technique can be found +elsewhere~\cite{paulson-jcs}, including proofs of an Internet +protocol~\cite{paulson-tls}. We must stress that the protocol discussed +in this chapter is trivial. There are only three messages; no keys are +exchanged; we merely have to prove that encrypted data remains secret. +Real world protocols are much longer and distribute many secrets to their +participants. To be realistic, the model has to include the possibility +of keys being lost dynamically due to carelessness. If those keys have +been used to encrypt other sensitive information, there may be cascading +losses. We may still be able to establish a bound on the losses and to +prove that other protocol runs function +correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow +the strategy illustrated above, but the subgoals can +be much bigger and there are more of them. +\index{protocols!security|)} +*} + +(*<*)end(*>*) diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Mon Jul 23 14:30:53 2007 +0200 +++ b/doc-src/TutorialI/Protocol/Public.thy Mon Jul 23 14:31:34 2007 +0200 @@ -6,20 +6,24 @@ Theory of Public Keys (common to all public-key protocols) Private and public keys; initial states of agents -*) - +*)(*<*) theory Public imports Event -uses ("Public_lemmas.ML") begin +begin +(*>*) -consts - pubK :: "agent => key" +text {* +The function +@{text pubK} maps agents to their public keys. The function +@{text priK} maps agents to their private keys. It is defined in terms of +@{text invKey} and @{text pubK} by a translation; therefore @{text priK} is +not a proper constant, so we declare it using \isacommand{syntax} +(cf.\ \S\ref{sec:syntax-translations}). +*} -syntax - priK :: "agent => key" - -translations (*BEWARE! expressions like (inj priK) will NOT work!*) - "priK x" == "invKey(pubK x)" - +consts pubK :: "agent => key" +syntax priK :: "agent => key" +translations "priK x" \ "invKey(pubK x)" +(*<*) primrec (*Agents know their private key and all public keys*) initState_Server: "initState Server = @@ -28,19 +32,139 @@ insert (Key (priK (Friend i))) (Key ` range pubK)" initState_Spy: "initState Spy = (Key`invKey`pubK`bad) Un (Key ` range pubK)" +(*>*) +text {* +\noindent +The set @{text bad} consists of those agents whose private keys are known to +the spy. + +Two axioms are asserted about the public-key cryptosystem. +No two agents have the same public key, and no private key equals +any public key. +*} axioms - (*Public keys are disjoint, and never clash with private keys*) inj_pubK: "inj pubK" priK_neq_pubK: "priK A ~= pubK B" +(*<*) +lemmas [iff] = inj_pubK [THEN inj_eq] -use "Public_lemmas.ML" +lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)" + apply safe + apply (drule_tac f=invKey in arg_cong) + apply simp + done + +lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym] + +lemma not_symKeys_pubK[iff]: "pubK A \ symKeys" + by (simp add: symKeys_def) + +lemma not_symKeys_priK[iff]: "priK A \ symKeys" + by (simp add: symKeys_def) + +lemma symKeys_neq_imp_neq: "(K \ symKeys) \ (K' \ symKeys) ==> K \ K'" + by blast + +lemma analz_symKeys_Decrypt: "[| Crypt K X \ analz H; K \ symKeys; Key K \ analz H |] + ==> X \ analz H" + by (auto simp add: symKeys_def) + + +(** "Image" equations that hold for injective functions **) + +lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)" + by auto + +(*holds because invKey is injective*) +lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)" + by auto + +lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)" + by auto + + +(** Rewrites should not refer to initState(Friend i) + -- not in normal form! **) + +lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}" + apply (unfold keysFor_def) + apply (induct C) + apply (auto intro: range_eqI) + done + + +(*** Function "spies" ***) + +(*Agents see their own private keys!*) +lemma priK_in_initState[iff]: "Key (priK A) : initState A" + by (induct A) auto + +(*All public keys are visible*) +lemma spies_pubK[iff]: "Key (pubK A) : spies evs" + by (induct evs) (simp_all add: imageI knows_Cons split: event.split) + +(*Spy sees private keys of bad agents!*) +lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs" + by (induct evs) (simp_all add: imageI knows_Cons split: event.split) + +lemmas [iff] = spies_pubK [THEN analz.Inj] + + +(*** Fresh nonces ***) + +lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)" + by (induct B) auto + +lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []" + by (simp add: used_Nil) + + +(*** Supply fresh nonces for possibility theorems. ***) + +(*In any trace, there is an upper bound N on the greatest nonce in use.*) +lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \ used evs" +apply (induct_tac "evs") +apply (rule_tac x = 0 in exI) +apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) +apply safe +apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ +done + +lemma Nonce_supply1: "EX N. Nonce N \ used evs" +by (rule Nonce_supply_lemma [THEN exE], blast) + +lemma Nonce_supply: "Nonce (@ N. Nonce N \ used evs) \ used evs" +apply (rule Nonce_supply_lemma [THEN exE]) +apply (rule someI, fast) +done + + +(*** Specialized rewriting for the analz_image_... theorems ***) + +lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H" + by blast + +lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C" + by blast + (*Specialized methods*) +(*Tactic for possibility theorems*) +ML {* +fun possibility_tac st = st |> + REPEAT (*omit used_Says so that Nonces start from different traces!*) + (ALLGOALS (simp_tac (simpset() delsimps [used_Says])) + THEN + REPEAT_FIRST (eq_assume_tac ORELSE' + resolve_tac [refl, conjI, @{thm Nonce_supply}])); +*} + method_setup possibility = {* Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} "for proving possibility theorems" end +(*>*) \ No newline at end of file diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/document/Event.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/document/Event.tex Mon Jul 23 14:31:34 2007 +0200 @@ -0,0 +1,518 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Event}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isamarkupsection{Event Traces \label{sec:events}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The system's behaviour is formalized as a set of traces of +\emph{events}. The most important event, \isa{Says\ A\ B\ X}, expresses +$A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$. +A trace is simply a list, constructed in reverse +using~\isa{{\isacharhash}}. Other event types include reception of messages (when +we want to make it explicit) and an agent's storing a fact. + +Sometimes the protocol requires an agent to generate a new nonce. The +probability that a 20-byte random number has appeared before is effectively +zero. To formalize this important property, the set \isa{used\ evs} +denotes the set of all items mentioned in the trace~\isa{evs}. +The function \isa{used} has a straightforward +recursive definition. Here is the case for \isa{Says} event: +\begin{isabelle}% +\ \ \ \ \ used\ {\isacharparenleft}Says\ A\ B\ X\ {\isacharhash}\ evs{\isacharparenright}\ {\isacharequal}\ parts\ {\isacharbraceleft}X{\isacharbraceright}\ {\isasymunion}\ used\ evs% +\end{isabelle} + +The function \isa{knows} formalizes an agent's knowledge. Mostly we only +care about the spy's knowledge, and \isa{knows\ Spy\ evs} is the set of items +available to the spy in the trace~\isa{evs}. Already in the empty trace, +the spy starts with some secrets at his disposal, such as the private keys +of compromised users. After each \isa{Says} event, the spy learns the +message that was sent: +\begin{isabelle}% +\ \ \ \ \ knows\ Spy\ {\isacharparenleft}Says\ A\ B\ X\ {\isacharhash}\ evs{\isacharparenright}\ {\isacharequal}\ insert\ X\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}% +\end{isabelle} +Combinations of functions express other important +sets of messages derived from~\isa{evs}: +\begin{itemize} +\item \isa{analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}} is everything that the spy could +learn by decryption +\item \isa{synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharparenright}} is everything that the spy +could generate +\end{itemize}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/document/Message.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/document/Message.tex Mon Jul 23 14:31:34 2007 +0200 @@ -0,0 +1,1638 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Message}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsection{Agents and Messages% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +All protocol specifications refer to a syntactic theory of messages. +Datatype +\isa{agent} introduces the constant \isa{Server} (a trusted central +machine, needed for some protocols), an infinite population of +friendly agents, and the~\isa{Spy}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ agent\ {\isacharequal}\ Server\ {\isacharbar}\ Friend\ nat\ {\isacharbar}\ Spy% +\begin{isamarkuptext}% +Keys are just natural numbers. Function \isa{invKey} maps a public key to +the matching private key, and vice versa:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{types}\isamarkupfalse% +\ key\ {\isacharequal}\ nat\isanewline +\isacommand{consts}\isamarkupfalse% +\ invKey\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}key{\isacharequal}{\isachargreater}key{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Datatype +\isa{msg} introduces the message forms, which include agent names, nonces, +keys, compound messages, and encryptions.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\isanewline +\ \ \ \ \ msg\ {\isacharequal}\ Agent\ \ agent\isanewline +\ \ \ \ \ \ \ \ \ {\isacharbar}\ Nonce\ \ nat\isanewline +\ \ \ \ \ \ \ \ \ {\isacharbar}\ Key\ \ \ \ key\isanewline +\ \ \ \ \ \ \ \ \ {\isacharbar}\ MPair\ \ msg\ msg\isanewline +\ \ \ \ \ \ \ \ \ {\isacharbar}\ Crypt\ \ key\ msg% +\begin{isamarkuptext}% +\noindent +The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ +abbreviates +$\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. + +Since datatype constructors are injective, we have the theorem +\begin{isabelle}% +Crypt\ K\ X\ {\isacharequal}\ Crypt\ K{\isacharprime}\ X{\isacharprime}\ {\isasymLongrightarrow}\ K\ {\isacharequal}\ K{\isacharprime}\ {\isasymand}\ X\ {\isacharequal}\ X{\isacharprime}% +\end{isabelle} +A ciphertext can be decrypted using only one key and +can yield only one plaintext. In the real world, decryption with the +wrong key succeeds but yields garbage. Our model of encryption is +realistic if encryption adds some redundancy to the plaintext, such as a +checksum, so that garbage can be detected.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsection{Modelling the Adversary% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The spy is part of the system and must be built into the model. He is +a malicious user who does not have to follow the protocol. He +watches the network and uses any keys he knows to decrypt messages. +Thus he accumulates additional keys and nonces. These he can use to +compose new messages, which he may send to anybody. + +Two functions enable us to formalize this behaviour: \isa{analz} and +\isa{synth}. Each function maps a sets of messages to another set of +messages. The set \isa{analz\ H} formalizes what the adversary can learn +from the set of messages~$H$. The closure properties of this set are +defined inductively.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ analz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set\ {\isasymRightarrow}\ msg\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ H\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{where}\isanewline +\ \ \ \ Inj\ {\isacharbrackleft}intro{\isacharcomma}simp{\isacharbrackright}\ {\isacharcolon}\ {\isachardoublequoteopen}X\ {\isasymin}\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ analz\ H{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ Fst{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ analz\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ analz\ H{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ Snd{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ analz\ H\ {\isasymLongrightarrow}\ Y\ {\isasymin}\ analz\ H{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ Decrypt\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt\ K\ X\ {\isasymin}\ analz\ H{\isacharsemicolon}\ Key{\isacharparenleft}invKey\ K{\isacharparenright}\ {\isasymin}\ analz\ H{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ X\ {\isasymin}\ analz\ H{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Note the \isa{Decrypt} rule: the spy can decrypt a +message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. +Properties proved by rule induction include the following: +\begin{isabelle}% +G\ {\isasymsubseteq}\ H\ {\isasymLongrightarrow}\ analz\ G\ {\isasymsubseteq}\ analz\ H\rulename{analz{\isacharunderscore}mono}\par\smallskip% +analz\ {\isacharparenleft}analz\ H{\isacharparenright}\ {\isacharequal}\ analz\ H\rulename{analz{\isacharunderscore}idem}% +\end{isabelle} + +The set of fake messages that an intruder could invent +starting from~\isa{H} is \isa{synth{\isacharparenleft}analz\ H{\isacharparenright}}, where \isa{synth\ H} +formalizes what the adversary can build from the set of messages~$H$.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ synth\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set\ {\isasymRightarrow}\ msg\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ H\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{where}\isanewline +\ \ \ \ Inj\ \ \ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}X\ {\isasymin}\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ Agent\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Agent\ agt\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ MPair\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Y\ {\isasymin}\ synth\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ Crypt\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Key{\isacharparenleft}K{\isacharparenright}\ {\isasymin}\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ Crypt\ K\ X\ {\isasymin}\ synth\ H{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The set includes all agent names. Nonces and keys are assumed to be +unguessable, so none are included beyond those already in~$H$. Two +elements of \isa{synth\ H} can be combined, and an element can be encrypted +using a key present in~$H$. + +Like \isa{analz}, this set operator is monotone and idempotent. It also +satisfies an interesting equation involving \isa{analz}: +\begin{isabelle}% +analz\ {\isacharparenleft}synth\ H{\isacharparenright}\ {\isacharequal}\ analz\ H\ {\isasymunion}\ synth\ H\rulename{analz{\isacharunderscore}synth}% +\end{isabelle} +Rule inversion plays a major role in reasoning about \isa{synth}, through +declarations such as this one:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% +\ Nonce{\isacharunderscore}synth\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Nonce\ n\ {\isasymin}\ synth\ H{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent +The resulting elimination rule replaces every assumption of the form +\isa{Nonce\ n\ {\isasymin}\ synth\ H} by \isa{Nonce\ n\ {\isasymin}\ H}, +expressing that a nonce cannot be guessed. + +A third operator, \isa{parts}, is useful for stating correctness +properties. The set +\isa{parts\ H} consists of the components of elements of~$H$. This set +includes~\isa{H} and is closed under the projections from a compound +message to its immediate parts. +Its definition resembles that of \isa{analz} except in the rule +corresponding to the constructor \isa{Crypt}: +\begin{isabelle}% +\ \ \ \ \ Crypt\ K\ X\ {\isasymin}\ parts\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ parts\ H% +\end{isabelle} +The body of an encrypted message is always regarded as part of it. We can +use \isa{parts} to express general well-formedness properties of a protocol, +for example, that an uncompromised agent's private key will never be +included as a component of any message.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/document/NS_Public.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex Mon Jul 23 14:31:34 2007 +0200 @@ -0,0 +1,517 @@ +% +\begin{isabellebody}% +\def\isabellecontext{NS{\isacharunderscore}Public}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupsection{Modelling the Protocol \label{sec:modelling}% +} +\isamarkuptrue% +% +\begin{figure} +\begin{isabelle} +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\ ns{\isacharunderscore}public\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}event\ list\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{where}\isanewline +\isanewline +\ \ \ Nil{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\ {\isacharbar}\ Fake{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ X\ {\isasymin}\ synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ Spy\ B\ X\ \ {\isacharhash}\ evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\ {\isacharbar}\ NS{\isadigit{1}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{1}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ Nonce\ NA\ {\isasymnotin}\ used\ evs{\isadigit{1}}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharhash}\ evs{\isadigit{1}}\ \ {\isasymin}\ \ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\ {\isacharbar}\ NS{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{2}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isadigit{2}}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharhash}\ evs{\isadigit{2}}\ \ {\isasymin}\ \ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\ {\isacharbar}\ NS{\isadigit{3}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{3}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isadigit{3}}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ Says\ B{\isacharprime}\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymin}\ set\ evs{\isadigit{3}}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isacharhash}\ evs{\isadigit{3}}\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}% +\end{isabelle} +\caption{An Inductive Protocol Definition}\label{fig:ns_public} +\end{figure} +% +\begin{isamarkuptext}% +Let us formalize the Needham-Schroeder public-key protocol, as corrected by +Lowe: +\begin{alignat*% +}{2} + &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ + &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ + &3.&\quad A\to B &: \comp{Nb}\sb{Kb} +\end{alignat*% +} + +Each protocol step is specified by a rule of an inductive definition. An +event trace has type \isa{event\ list}, so we declare the constant +\isa{ns{\isacharunderscore}public} to be a set of such traces. + +Figure~\ref{fig:ns_public} presents the inductive definition. The +\isa{Nil} rule introduces the empty trace. The \isa{Fake} rule models the +adversary's sending a message built from components taken from past +traffic, expressed using the functions \isa{synth} and +\isa{analz}. +The next three rules model how honest agents would perform the three +protocol steps. + +Here is a detailed explanation of rule \isa{NS{\isadigit{2}}}. +A trace containing an event of the form +\begin{isabelle}% +\ \ \ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}% +\end{isabelle} +may be extended by an event of the form +\begin{isabelle}% +\ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}% +\end{isabelle} +where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}. +Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not +know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather +than simply \isa{evs} helps us know where we are in a proof after many +case-splits: every subgoal mentioning \isa{evs{\isadigit{2}}} involves message~2 of the +protocol. + +Benefits of this approach are simplicity and clarity. The semantic model +is set theory, proofs are by induction and the translation from the informal +notation to the inductive rules is straightforward.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Proving Elementary Properties \label{sec:regularity}% +} +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +Secrecy properties can be hard to prove. The conclusion of a typical +secrecy theorem is +\isa{X\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}}. The difficulty arises from +having to reason about \isa{analz}, or less formally, showing that the spy +can never learn~\isa{X}. Much easier is to prove that \isa{X} can never +occur at all. Such \emph{regularity} properties are typically expressed +using \isa{parts} rather than \isa{analz}. + +The following lemma states that \isa{A}'s private key is potentially +known to the spy if and only if \isa{A} belongs to the set \isa{bad} of +compromised agents. The statement uses \isa{parts}: the very presence of +\isa{A}'s private key in a message, whether protected by encryption or +not, is enough to confirm that \isa{A} is compromised. The proof, like +nearly all protocol proofs, is by induction over traces.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ Spy{\isacharunderscore}see{\isacharunderscore}priK\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline +\ \ \ \ \ \ {\isachardoublequoteopen}evs\ {\isasymin}\ ns{\isacharunderscore}public\isanewline +\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% +\begin{isamarkuptxt}% +The induction yields five subgoals, one for each rule in the definition of +\isa{ns{\isacharunderscore}public}. The idea is to prove that the protocol property holds initially +(rule \isa{Nil}), is preserved by each of the legitimate protocol steps (rules +\isa{NS{\isadigit{1}}}--\isa{{\isadigit{3}}}), and even is preserved in the face of anything the +spy can do (rule \isa{Fake}). + +The proof is trivial. No legitimate protocol rule sends any keys +at all, so only \isa{Fake} is relevant. Indeed, simplification leaves +only the \isa{Fake} case, as indicated by the variable name \isa{evsf}: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}evsf\ X{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }X\ {\isasymin}\ synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}insert\ X\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }{\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The \isa{Fake} case is proved automatically. If +\isa{priK\ A} is in the extended trace then either (1) it was already in the +original trace or (2) it was +generated by the spy, who must have known this key already. +Either way, the induction hypothesis applies. + +\emph{Unicity} lemmas are regularity lemmas stating that specified items +can occur only once in a trace. The following lemma states that a nonce +cannot be used both as $Na$ and as $Nb$ unless +it is known to the spy. Intuitively, it holds because honest agents +always choose fresh values as nonces; only the spy might reuse a value, +and he doesn't know this particular value. The proof script is short: +induction, simplification, \isa{blast}. The first line uses the rule +\isa{rev{\isacharunderscore}mp} to prepare the induction by moving two assumptions into the +induction formula.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ no{\isacharunderscore}nonce{\isacharunderscore}NS{\isadigit{1}}{\isacharunderscore}NS{\isadigit{2}}{\isacharcolon}\isanewline +\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt\ {\isacharparenleft}pubK\ C{\isacharparenright}\ {\isasymlbrace}NA{\isacharprime}{\isacharcomma}\ Nonce\ NA{\isacharcomma}\ Agent\ D{\isasymrbrace}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ Nonce\ NA\ {\isasymin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ rev{\isacharunderscore}mp{\isacharcomma}\ erule\ rev{\isacharunderscore}mp{\isacharparenright}\isanewline +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}blast\ intro{\isacharcolon}\ analz{\isacharunderscore}insertI{\isacharparenright}{\isacharplus}\isanewline +\isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The following unicity lemma states that, if \isa{NA} is secret, then its +appearance in any instance of message~1 determines the other components. +The proof is similar to the previous one.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ unique{\isacharunderscore}NA{\isacharcolon}\isanewline +\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt{\isacharparenleft}pubK\ B{\isacharparenright}\ \ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A\ {\isasymrbrace}\ {\isasymin}\ parts{\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ Crypt{\isacharparenleft}pubK\ B{\isacharprime}{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isacharprime}{\isasymrbrace}\ {\isasymin}\ parts{\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ Nonce\ NA\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline +\ \ \ \ \ \ {\isasymLongrightarrow}\ A{\isacharequal}A{\isacharprime}\ {\isasymand}\ B{\isacharequal}B{\isacharprime}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsection{Proving Secrecy Theorems \label{sec:secrecy}% +} +\isamarkuptrue% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The secrecy theorems for Bob (the second participant) are especially +important because they fail for the original protocol. The following +theorem states that if Bob sends message~2 to Alice, and both agents are +uncompromised, then Bob's nonce will never reach the spy.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{theorem}\isamarkupfalse% +\ Spy{\isacharunderscore}not{\isacharunderscore}see{\isacharunderscore}NB\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\isanewline +\ {\isachardoublequoteopen}{\isasymlbrakk}Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline +\ \ \ A\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline +\ \ {\isasymLongrightarrow}\ Nonce\ NB\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +To prove it, we must formulate the induction properly (one of the +assumptions mentions~\isa{evs}), apply induction, and simplify:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +\ {\isacharparenleft}erule\ rev{\isacharunderscore}mp{\isacharcomma}\ erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% +\begin{isamarkuptxt}% +The proof states are too complicated to present in full. +Let's examine the simplest subgoal, that for message~1. The following +event has just occurred: +\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \] +The variables above have been primed because this step +belongs to a different run from that referred to in the theorem +statement --- the theorem +refers to a past instance of message~2, while this subgoal +concerns message~1 being sent just now. +In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$ +we have \isa{Ba} and~\isa{NAa}: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}evs{\isadigit{1}}\ NAa\ Ba{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}A\ {\isasymnotin}\ bad{\isacharsemicolon}\ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ evs{\isadigit{1}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isasymin}\ set\ evs{\isadigit{1}}\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Nonce\ NB\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Nonce\ NAa\ {\isasymnotin}\ used\ evs{\isadigit{1}}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Ba\ {\isasymin}\ bad\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }{\isasymin}\ set\ evs{\isadigit{1}}\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }NB\ {\isasymnoteq}\ NAa% +\end{isabelle} +The simplifier has used a +default simplification rule that does a case +analysis for each encrypted message on whether or not the decryption key +is compromised. +\begin{isabelle}% +analz\ {\isacharparenleft}insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ H{\isacharparenright}\ {\isacharequal}\isanewline +{\isacharparenleft}if\ Key\ {\isacharparenleft}invKey\ K{\isacharparenright}\ {\isasymin}\ analz\ H\isanewline +\isaindent{{\isacharparenleft}}then\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ {\isacharparenleft}insert\ X\ H{\isacharparenright}{\isacharparenright}\isanewline +\isaindent{{\isacharparenleft}}else\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ H{\isacharparenright}{\isacharparenright}\rulename{analz{\isacharunderscore}Crypt{\isacharunderscore}if}% +\end{isabelle} +The simplifier has also used \isa{Spy{\isacharunderscore}see{\isacharunderscore}priK}, proved in +{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ {\isasymin}\ bad}. + +Recall that this subgoal concerns the case +where the last message to be sent was +\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \] +This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised, +allowing the spy to decrypt the message. The Isabelle subgoal says +precisely this, if we allow for its choice of variable names. +Proving \isa{NB\ {\isasymnoteq}\ NAa} is easy: \isa{NB} was +sent earlier, while \isa{NAa} is fresh; formally, we have +the assumption \isa{Nonce\ NAa\ {\isasymnotin}\ used\ evs{\isadigit{1}}}. + +Note that our reasoning concerned \isa{B}'s participation in another +run. Agents may engage in several runs concurrently, and some attacks work +by interleaving the messages of two runs. With model checking, this +possibility can cause a state-space explosion, and for us it +certainly complicates proofs. The biggest subgoal concerns message~2. It +splits into several cases, such as whether or not the message just sent is +the very message mentioned in the theorem statement. +Some of the cases are proved by unicity, others by +the induction hypothesis. For all those complications, the proofs are +automatic by \isa{blast} with the theorem \isa{no{\isacharunderscore}nonce{\isacharunderscore}NS{\isadigit{1}}{\isacharunderscore}NS{\isadigit{2}}}. + +The remaining theorems about the protocol are not hard to prove. The +following one asserts a form of \emph{authenticity}: if +\isa{B} has sent an instance of message~2 to~\isa{A} and has received the +expected reply, then that reply really originated with~\isa{A}. The +proof is a simple induction.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isacommand{theorem}\isamarkupfalse% +\ B{\isacharunderscore}trusts{\isacharunderscore}NS{\isadigit{3}}{\isacharcolon}\isanewline +\ {\isachardoublequoteopen}{\isasymlbrakk}Says\ B\ A\ \ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline +\ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline +\ \ \ A\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline +\ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ evs{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +From similar assumptions, we can prove that \isa{A} started the protocol +run by sending an instance of message~1 involving the nonce~\isa{NA}\@. +For this theorem, the conclusion is +\begin{isabelle}% +Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs% +\end{isabelle} +Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA} +remains secret and that message~2 really originates with~\isa{B}. Even the +flawed protocol establishes these properties for~\isa{A}; +the flaw only harms the second participant. + +\medskip + +Detailed information on this protocol verification technique can be found +elsewhere~\cite{paulson-jcs}, including proofs of an Internet +protocol~\cite{paulson-tls}. We must stress that the protocol discussed +in this chapter is trivial. There are only three messages; no keys are +exchanged; we merely have to prove that encrypted data remains secret. +Real world protocols are much longer and distribute many secrets to their +participants. To be realistic, the model has to include the possibility +of keys being lost dynamically due to carelessness. If those keys have +been used to encrypt other sensitive information, there may be cascading +losses. We may still be able to establish a bound on the losses and to +prove that other protocol runs function +correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow +the strategy illustrated above, but the subgoals can +be much bigger and there are more of them. +\index{protocols!security|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/document/Public.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/document/Public.tex Mon Jul 23 14:31:34 2007 +0200 @@ -0,0 +1,323 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Public}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\begin{isamarkuptext}% +The function +\isa{pubK} maps agents to their public keys. The function +\isa{priK} maps agents to their private keys. It is defined in terms of +\isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is +not a proper constant, so we declare it using \isacommand{syntax} +(cf.\ \S\ref{sec:syntax-translations}).% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline +\isacommand{syntax}\isamarkupfalse% +\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline +\isacommand{translations}\isamarkupfalse% +\ {\isachardoublequoteopen}priK\ x{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent +The set \isa{bad} consists of those agents whose private keys are known to +the spy. + +Two axioms are asserted about the public-key cryptosystem. +No two agents have the same public key, and no private key equals +any public key.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{axioms}\isamarkupfalse% +\isanewline +\ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline +\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isachartilde}{\isacharequal}\ pubK\ B{\isachardoublequoteclose}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/protocol.tex --- a/doc-src/TutorialI/Protocol/protocol.tex Mon Jul 23 14:30:53 2007 +0200 +++ b/doc-src/TutorialI/Protocol/protocol.tex Mon Jul 23 14:31:34 2007 +0200 @@ -130,518 +130,7 @@ \index{Needham-Schroeder protocol|)} -\section{Agents and Messages} - -All protocol specifications refer to a syntactic theory of messages. -Datatype -\isa{agent} introduces the constant \isa{Server} (a trusted central -machine, needed for some protocols), an infinite population of -friendly agents, and the~\isa{Spy}: -\begin{isabelle} -\isacommand{datatype}\ agent\ =\ Server\ |\ Friend\ nat\ |\ Spy -\end{isabelle} -% -Keys are just natural numbers. Function \isa{invKey} maps a public key to -the matching private key, and vice versa: -\begin{isabelle} -\isacommand{types}\ key\ =\ nat\isanewline -\isacommand{consts}\ invKey\ ::\ "key=>key" -\end{isabelle} -Datatype -\isa{msg} introduces the message forms, which include agent names, nonces, -keys, compound messages, and encryptions. -\begin{isabelle} -\isacommand{datatype}\isanewline -\ \ \ \ \ msg\ =\ Agent\ \ agent\ \ \ \ \ \isanewline -\ \ \ \ \ \ \ \ \ |\ Nonce\ \ nat\ \ \ \ \ \ \ \isanewline -\ \ \ \ \ \ \ \ \ |\ Key\ \ \ \ key\ \ \ \ \ \ \ \isanewline -\ \ \ \ \ \ \ \ \ |\ MPair\ \ msg\ msg\ \ \ \isanewline -\ \ \ \ \ \ \ \ \ |\ Crypt\ \ key\ msg\ \ \ \isanewline -\end{isabelle} -% -The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ -abbreviates -$\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. - -Since datatype constructors are injective, we have the theorem -\begin{isabelle} -Crypt K X = Crypt K' X' \isasymLongrightarrow\ K=K' \isasymand\ X=X'. -\end{isabelle} -A ciphertext can be decrypted using only one key and -can yield only one plaintext. In the real world, decryption with the -wrong key succeeds but yields garbage. Our model of encryption is -realistic if encryption adds some redundancy to the plaintext, such as a -checksum, so that garbage can be detected. - - -\section{Modelling the Adversary} - -The spy is part of the system and must be built into the model. He is -a malicious user who does not have to follow the protocol. He -watches the network and uses any keys he knows to decrypt messages. -Thus he accumulates additional keys and nonces. These he can use to -compose new messages, which he may send to anybody. - -Two functions enable us to formalize this behaviour: \isa{analz} and -\isa{synth}. Each function maps a sets of messages to another set of -messages. The set \isa{analz H} formalizes what the adversary can learn -from the set of messages~$H$. The closure properties of this set are -defined inductively. -\begin{isabelle} -\isacommand{consts}\ \ analz\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline -\isacommand{inductive}\ "analz\ H"\isanewline -\ \ \isakeyword{intros}\ \isanewline -\ \ \ \ Inj\ [intro,simp]\ :\ "X\ \isasymin \ H\ -\isasymLongrightarrow\ X\ -\isasymin -\ analz\ H"\isanewline -\ \ \ \ Fst:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ -analz\ H\ -\isasymLongrightarrow\ X\ \isasymin \ analz\ H"\isanewline -\ \ \ \ Snd:\ \ \ \ \ "{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ analz\ H\ -\isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline -\ \ \ \ Decrypt\ [dest]:\ \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\ -K)\ \isasymin\ analz\ H\isasymrbrakk\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H" -\end{isabelle} -% -Note the \isa{Decrypt} rule: the spy can decrypt a -message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. -Properties proved by rule induction include the following: -\begin{isabelle} -G\isasymsubseteq H\ \isasymLongrightarrow\ analz(G)\ \isasymsubseteq\ -analz(H) -\rulename{analz_mono}\isanewline -analz (analz H) = analz H -\rulename{analz_idem} -\end{isabelle} - -The set of fake messages that an intruder could invent -starting from~\isa{H} is \isa{synth(analz~H)}, where \isa{synth H} -formalizes what the adversary can build from the set of messages~$H$. -\begin{isabelle} -\isacommand{consts}\ \ synth\ \ \ ::\ "msg\ set\ =>\ msg\ set"\isanewline -\isacommand{inductive}\ "synth\ H"\isanewline -\ \ \isakeyword{intros}\ \isanewline -\ \ \ \ Inj\ \ \ [intro]:\ "X\ \isasymin \ H\ \isasymLongrightarrow\ -X\ \isasymin \ synth\ H"\isanewline -\ \ \ \ Agent\ [intro]:\ "Agent\ agt\ \isasymin \ synth\ H"\isanewline -\ \ \ \ MPair\ [intro]:\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Y\ \isasymin -\ synth\ H\isasymrbrakk\ \isasymLongrightarrow\ -{\isasymlbrace}X,Y\isasymrbrace \ \isasymin \ synth\ H"\isanewline -\ \ \ \ Crypt\ [intro]:\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}X\ \isasymin \ synth\ H;\ \ Key K\ -\isasymin \ H\isasymrbrakk\ \isasymLongrightarrow\ Crypt\ K\ X\ -\isasymin \ synth\ H" -\end{isabelle} -The set includes all agent names. Nonces and keys are assumed to be -unguessable, so none are included beyond those already in~$H$. Two -elements of \isa{synth H} can be combined, and an element can be encrypted -using a key present in~$H$. - -Like \isa{analz}, this set operator is monotone and idempotent. It also -satisfies an interesting equation involving \isa{analz}: -\begin{isabelle} -analz (synth H)\ =\ analz H\ \isasymunion\ synth H -\rulename{analz_synth} -\end{isabelle} -% -Rule inversion plays a major role in reasoning about \isa{synth}, through -declarations such as this one: -\begin{isabelle} -\isacommand{inductive\_cases}\ Nonce_synth\ [elim!]:\ "Nonce\ n\ \isasymin -\ synth\ H" -\end{isabelle} -% -The resulting elimination rule replaces every assumption of the form -\isa{Nonce\ n\ \isasymin \ synth\ H} by \isa{Nonce\ n\ -\isasymin \ H}, expressing that a nonce cannot be guessed. -%The theory also uses rule inversion with constructors \isa{Key}, \isa{Crypt} -%and \isa{MPair} (message pairing). - -% -A third operator, \isa{parts}, is useful for stating correctness -properties. The set -\isa{parts H} consists of the components of elements of~$H$. This set -includes~\isa{H} and is closed under the projections from a compound -message to its immediate parts. -Its definition resembles that of \isa{analz} except in the rule -corresponding to the constructor \isa{Crypt}: -\begin{isabelle} -\ \ \ \ \ Crypt\ K\ X\ \isasymin \ parts\ H\ \isasymLongrightarrow\ X\ -\isasymin \ parts\ H -\end{isabelle} -The body of an encrypted message is always regarded as part of it. We can -use \isa{parts} to express general well-formedness properties of a protocol, -for example, that an uncompromised agent's private key will never be -included as a component of any message. - - -\section{Event Traces}\label{sec:events} - -The system's behaviour is formalized as a set of traces of -\emph{events}. The most important event, \isa{Says~A~B~X}, expresses -$A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$. -A trace is simply a list, constructed in reverse -using~\isa{\#}. Other event types include reception of messages (when -we want to make it explicit) and an agent's storing a fact. - -Sometimes the protocol requires an agent to generate a new nonce. The -probability that a 20-byte random number has appeared before is effectively -zero. To formalize this important property, the set \isa{used evs} -denotes the set of all items mentioned in the trace~\isa{evs}. -The function \isa{used} has a straightforward -recursive definition. Here is the case for \isa{Says} event: -\begin{isabelle} -\ \ \ \ \ used\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\ \isacharbraceleft -X\isacharbraceright \ \isasymunion\ (used\ evs) -\end{isabelle} - -The function \isa{knows} formalizes an agent's knowledge. Mostly we only -care about the spy's knowledge, and \isa{knows Spy evs} is the set of items -available to the spy in the trace~\isa{evs}. Already in the empty trace, -the spy starts with some secrets at his disposal, such as the private keys -of compromised users. After each \isa{Says} event, the spy learns the -message that was sent: -\begin{isabelle} -\ \ \ \ \ knows\ Spy\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ insert X\ (knows\ Spy\ evs) -\end{isabelle} -% -Combinations of functions express other important -sets of messages derived from~\isa{evs}: -\begin{itemize} -\item \isa{analz (knows Spy evs)} is everything that the spy could -learn by decryption -\item \isa{synth (analz (knows Spy evs))} is everything that the spy -could generate -\end{itemize} - -The function -\isa{pubK} maps agents to their public keys. The function -\isa{priK} maps agents to their private keys. It is defined in terms of -\isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is -not a proper constant, so we declare it using \isacommand{syntax} -(cf.\ \S\ref{sec:syntax-translations}). -\begin{isabelle} -\isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline -\isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline -\isacommand{translations}\ \ \ \ "priK\ x"\ \ \isasymrightleftharpoons\ \ "invKey(pubK\ x)" -\end{isabelle} -The set \isa{bad} consists of those agents whose private keys are known to -the spy. - -Two axioms are asserted about the public-key cryptosystem. -No two agents have the same public key, and no private key equals -any public key. -\begin{isabelle} -\isacommand{axioms}\isanewline -\ \ inj_pubK:\ \ \ \ \ \ \ \ "inj\ pubK"\isanewline -\ \ priK_neq_pubK:\ \ \ "priK\ A\ \isasymnoteq\ pubK\ B" -\end{isabelle} - - - - - -\section{Modelling the Protocol}\label{sec:modelling} - -Let us formalize the Needham-Schroeder public-key protocol, as corrected by -Lowe: -\begin{alignat*}{2} - &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ - &2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ - &3.&\quad A\to B &: \comp{Nb}\sb{Kb} -\end{alignat*} - -Each protocol step is specified by a rule of an inductive definition. An -event trace has type \isa{event list}, so we declare the constant -\isa{ns_public} to be a set of such traces. -\begin{isabelle} -\isacommand{consts}\ \ ns_public\ \ ::\ "event\ list\ set" -\end{isabelle} - -\begin{figure} -\begin{isabelle} -\isacommand{inductive}\ ns_public\isanewline -\ \ \isakeyword{intros}\ \isanewline -\ \ \ \ \ \ \ \ \ \isanewline -\ \ \ Nil:\ \ "[]\ \isasymin \ ns_public"\isanewline -\isanewline -\ \ \ \ \ \ \ \ \ \isanewline -\ \ \ Fake:\ "\isasymlbrakk evsf\ \isasymin \ ns_public;\ \ X\ \isasymin \ synth\ (analz\ (knows\ Spy\ evsf))\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ Spy\ B\ X\ \ \#\ evsf\ \isasymin \ ns_public"\isanewline -\isanewline -\ \ \ \ \ \ \ \ \ \isanewline -\ \ \ NS1:\ \ "\isasymlbrakk evs1\ \isasymin \ ns_public;\ \ Nonce\ NA\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs1\ \ \isasymin \ \ ns_public"\isanewline -\isanewline -\ \ \ \ \ \ \ \ \ \isanewline -\ \ \ NS2:\ \ "\isasymlbrakk evs2\ \isasymin \ ns_public;\ \ Nonce\ NB\ \isasymnotin \ used\ evs2;\isanewline -\ \ \ \ \ \ \ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs2\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \#\ evs2\ \ \isasymin \ \ ns_public"\isanewline -\isanewline -\ \ \ \ \ \ \ \ \ \isanewline -\ \ \ NS3:\ \ "\isasymlbrakk evs3\ \isasymin \ ns_public;\isanewline -\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ A\isasymrbrace )\ \isasymin \ set\ evs3;\isanewline -\ \ \ \ \ \ \ \ \ \ \ Says\ B'\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymin \ set\ evs3\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \#\ evs3\ \isasymin \ -ns_public" -\end{isabelle} -\caption{An Inductive Protocol Definition}\label{fig:ns_public} -\end{figure} - -Figure~\ref{fig:ns_public} presents the inductive definition. The -\isa{Nil} rule introduces the empty trace. The \isa{Fake} rule models the -adversary's sending a message built from components taken from past -traffic, expressed using the functions \isa{synth} and -\isa{analz}. -The next three rules model how honest agents would perform the three -protocol steps. - -Here is a detailed explanation of rule \isa{NS2}. -A trace containing an event of the form -\begin{isabelle} -\ \ \ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ -NA,\ Agent\ A\isasymrbrace) -\end{isabelle} -% -may be extended by an event of the form -\begin{isabelle} -\ \ \ \ \ Says\ B\ A\ (Crypt\ (pubK\ A)\ -\isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace) -\end{isabelle} -where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ \isasymnotin \ used\ evs2}. -Writing the sender as \isa{A'} indicates that \isa{B} does not -know who sent the message. Calling the trace variable \isa{evs2} rather -than simply \isa{evs} helps us know where we are in a proof after many -case-splits: every subgoal mentioning \isa{evs2} involves message~2 of the -protocol. - -Benefits of this approach are simplicity and clarity. The semantic model -is set theory, proofs are by induction and the translation from the informal -notation to the inductive rules is straightforward. - - -\section{Proving Elementary Properties}\label{sec:regularity} - -Secrecy properties can be hard to prove. The conclusion of a typical -secrecy theorem is -\isa{X\ \isasymnotin\ analz (knows Spy evs)}. The difficulty arises from -having to reason about \isa{analz}, or less formally, showing that the spy -can never learn~\isa{X}. Much easier is to prove that \isa{X} can never -occur at all. Such \emph{regularity} properties are typically expressed -using \isa{parts} rather than \isa{analz}. - -The following lemma states that \isa{A}'s private key is potentially -known to the spy if and only if \isa{A} belongs to the set \isa{bad} of -compromised agents. The statement uses \isa{parts}: the very presence of -\isa{A}'s private key in a message, whether protected by encryption or -not, is enough to confirm that \isa{A} is compromised. The proof, like -nearly all protocol proofs, is by induction over traces. -\begin{isabelle} -\isacommand{lemma}\ Spy_see_priK\ [simp]:\ \isanewline -\ \ \ \ \ \ "evs\ \isasymin \ ns_public\isanewline -\ \ \ \ \ \ \ \isasymLongrightarrow \ -(Key\ (priK\ A)\ \isasymin \ parts\ (knows\ Spy\ evs))\ =\ (A\ \isasymin \ -bad)"\isanewline -\isacommand{apply}\ (erule\ ns_public.induct,\ simp_all) -\end{isabelle} -% -The induction yields five subgoals, one for each rule in the definition of -\isa{ns_public}. The idea is to prove that -the protocol property holds initially (rule -\isa{Nil}), is preserved by each of the legitimate protocol steps (rules -\isa{NS1}--\isa{3}), and even is preserved in the face of anything the -spy can do (rule -\isa{Fake}). - -The proof is trivial. No legitimate protocol rule sends any keys -at all, so only \isa{Fake} is relevant. Indeed, -simplification leaves only the \isa{Fake} case, as indicated by the -variable name -\isa{evsf}: -\begin{isabelle} -\ 1.\ \isasymAnd X\ evsf.\isanewline -\isaindent{\ 1.\ \ \ \ }\isasymlbrakk evsf\ \isasymin \ ns_public;\isanewline -\isaindent{\ 1.\ \ \ \ \ \ \ }(Key\ (priK\ A)\ \isasymin \ parts\ (knows\ Spy\ evsf))\ =\ (A\ \isasymin \ bad);\isanewline -\isaindent{\ 1.\ \ \ \ \ \ \ }X\ \isasymin \ synth\ (analz\ (knows\ Spy\ evsf))\isasymrbrakk \isanewline -\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ (Key\ (priK\ A)\ \isasymin \ parts\ (insert\ X\ (knows\ Spy\ evsf)))\ =\isanewline -\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }(A\ \isasymin \ -bad)\isanewline -\isacommand{by}\ blast -\end{isabelle} -% -The \isa{Fake} case is proved automatically. If -\isa{priK~A} is in the extended trace then either (1) it was already in the -original trace or (2) it was -generated by the spy, who must have known this key already. -Either way, the induction hypothesis applies. - -\emph{Unicity} lemmas are regularity lemmas stating that specified items -can occur only once in a trace. The following lemma states that a nonce -cannot be used both as $Na$ and as $Nb$ unless -it is known to the spy. Intuitively, it holds because honest agents -always choose fresh values as nonces; only the spy might reuse a value, -and he doesn't know this particular value. The proof script is short: -induction, simplification, \isa{blast}. The first line uses the rule -\isa{rev_mp} to prepare the induction by moving two assumptions into the -induction formula. -\begin{isabelle} -\isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline -\ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\ -NA,\ Agent\ D\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\ -evs);\isanewline -\ \ \ \ \ \ Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ -A\isasymrbrace \ \isasymin \ parts\ (knows\ Spy\ evs);\isanewline -\ \ \ \ \ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline -\ \ \ \ \ \isasymLongrightarrow \ Nonce\ NA\ \isasymin \ analz\ (knows\ -Spy\ evs)"\isanewline -\isacommand{apply}\ (erule\ rev_mp,\ erule\ rev_mp)\isanewline -\isacommand{apply}\ (erule\ ns_public.induct,\ simp_all)\isanewline -\isacommand{apply}\ (blast\ intro:\ analz_insertI)+\isanewline -\isacommand{done} -\end{isabelle} - -The following unicity lemma states that, if \isa{NA} is secret, then its -appearance in any instance of message~1 determines the other components. -The proof is similar to the previous one. -\begin{isabelle} -\isacommand{lemma}\ unique_NA:\ \isanewline -\ \ \ \ \ "\isasymlbrakk Crypt(pubK\ B)\ \ \isasymlbrace Nonce\ NA,\ Agent\ A\ \isasymrbrace \ \isasymin \ parts(knows\ Spy\ evs);\ \ \isanewline -\ \ \ \ \ \ \ Crypt(pubK\ B')\ \isasymlbrace Nonce\ NA,\ Agent\ A'\isasymrbrace \ \isasymin \ parts(knows\ Spy\ evs);\ \ \isanewline -\ \ \ \ \ \ \ Nonce\ NA\ \isasymnotin \ analz\ (knows\ Spy\ evs);\ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline -\ \ \ \ \ \ \isasymLongrightarrow \ A=A'\ \isasymand \ B=B'" -\end{isabelle} - - -\section{Proving Secrecy Theorems}\label{sec:secrecy} - -The secrecy theorems for Bob (the second participant) are especially -important because they fail for the original protocol. The following -theorem states that if Bob sends message~2 to Alice, and both agents are -uncompromised, then Bob's nonce will never reach the spy. -\begin{isabelle} -\isacommand{theorem}\ Spy_not_see_NB\ [dest]:\isanewline -\ "\isasymlbrakk Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline -\ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \isanewline -\ \ \isasymLongrightarrow \ Nonce\ NB\ \isasymnotin \ analz\ (knows\ Spy\ evs)" -\end{isabelle} -% -To prove it, we must formulate the induction properly (one of the -assumptions mentions~\isa{evs}), apply induction, and simplify: -\begin{isabelle} -\isacommand{apply}\ (erule\ rev_mp,\ erule\ ns_public.induct,\ simp_all) -\end{isabelle} -% -The proof states are too complicated to present in full. -Let's examine the simplest subgoal, that for message~1. The following -event has just occurred: -\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \] -The variables above have been primed because this step -belongs to a different run from that referred to in the theorem -statement --- the theorem -refers to a past instance of message~2, while this subgoal -concerns message~1 being sent just now. -In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$ -we have \isa{Ba} and~\isa{NAa}: -\begin{isabelle} -\ 1.\ \isasymAnd Ba\ NAa\ evs1.\isanewline -\isaindent{\ 1.\ \ \ \ }\isasymlbrakk A\ \isasymnotin \ bad;\ B\ \isasymnotin \ bad;\ evs1\ \isasymin \ ns_public;\isanewline -\isaindent{\ 1.\ \ \ \ \ \ \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline -\isaindent{\ 1.\ \ \ \ \ \ \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline -\isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NB\ \isasymnotin \ analz\ (knows\ Spy\ evs1);\isanewline -\isaindent{\ 1.\ \ \ \ \ \ \ }Nonce\ NAa\ \isasymnotin \ used\ evs1\isasymrbrakk \isanewline -\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Ba\ \isasymin \ bad\ \isasymlongrightarrow \isanewline -\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Says\ B\ A\ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\isanewline -\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }\isasymin \ set\ evs1\ \isasymlongrightarrow \isanewline -\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }NB\ \isasymnoteq \ NAa -\end{isabelle} -% -The simplifier has used a -default simplification rule that does a case -analysis for each encrypted message on whether or not the decryption key -is compromised. -\begin{isabelle} -analz\ (insert\ (Crypt\ K\ X)\ H)\ =\isanewline -\ (if\ Key\ (invKey\ K)\ \isasymin \ analz\ H\isanewline -\ \ then\ insert\ -(Crypt\ K\ X)\ (anal\ z\ (insert\ X\ H))\isanewline -\ \ else\ insert\ (Crypt\ K\ X)\ (analz\ H)) -\rulename{analz_Crypt_if} -\end{isabelle} -The simplifier has also used \isa{Spy_see_priK}, proved in -{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ \isasymin \ bad}. - -Recall that this subgoal concerns the case -where the last message to be sent was -\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \] -This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised, -allowing the spy to decrypt the message. The Isabelle subgoal says -precisely this, if we allow for its choice of variable names. -Proving \isa{NB\ \isasymnoteq \ NAa} is easy: \isa{NB} was -sent earlier, while \isa{NAa} is fresh; formally, we have -the assumption -\isa{Nonce\ NAa\ \isasymnotin \ used\ evs1}. - -Note that our reasoning concerned \isa{B}'s participation in another -run. Agents may engage in several runs concurrently, and some attacks work -by interleaving the messages of two runs. With model checking, this -possibility can cause a state-space explosion, and for us it -certainly complicates proofs. The biggest subgoal concerns message~2. It -splits into several cases, such as whether or not the message just sent is -the very message mentioned in the theorem statement. -Some of the cases are proved by unicity, others by -the induction hypothesis. For all those complications, the proofs are -automatic by \isa{blast} with the theorem \isa{no_nonce_NS1_NS2}. - -The remaining theorems about the protocol are not hard to prove. The -following one asserts a form of \emph{authenticity}: if -\isa{B} has sent an instance of message~2 to~\isa{A} and has received the -expected reply, then that reply really originated with~\isa{A}. The -proof is a simple induction. -\begin{isabelle} -\isacommand{theorem}\ B_trusts_NS3:\isanewline -\ "\isasymlbrakk Says\ B\ A\ \ (Crypt\ (pubK\ A)\ \isasymlbrace Nonce\ NA,\ Nonce\ NB,\ Agent\ B\isasymrbrace )\ \isasymin \ set\ evs;\isanewline -\ \ \ Says\ A'\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ evs;\ \isanewline -\ \ \ A\ \isasymnotin \ bad;\ \ B\ \isasymnotin \ bad;\ \ evs\ \isasymin \ ns_public\isasymrbrakk \ \ \ \ \ \ \ \ \isanewline -\ \ \isasymLongrightarrow \ Says\ A\ B\ (Crypt\ (pubK\ B)\ (Nonce\ NB))\ \isasymin \ set\ -evs" -\end{isabelle} - -From similar assumptions, we can prove that \isa{A} started the protocol -run by sending an instance of message~1 involving the nonce~\isa{NA}\@. -For this theorem, the conclusion is -\begin{isabelle} -\ \ \ \ \ Says\ A\ B\ (Crypt\ (pubK\ B)\ \isasymlbrace Nonce\ NA,\ Agent\ -A\isasymrbrace )\ \isasymin \ set\ evs -\end{isabelle} -% -Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA} -remains secret and that message~2 really originates with~\isa{B}. Even the -flawed protocol establishes these properties for~\isa{A}; -the flaw only harms the second participant. - -\medskip - -Detailed information on this protocol verification technique can be found -elsewhere~\cite{paulson-jcs}, including proofs of an Internet -protocol~\cite{paulson-tls}. We must stress that the protocol discussed -in this chapter is trivial. There are only three messages; no keys are -exchanged; we merely have to prove that encrypted data remains secret. -Real world protocols are much longer and distribute many secrets to their -participants. To be realistic, the model has to include the possibility -of keys being lost dynamically due to carelessness. If those keys have -been used to encrypt other sensitive information, there may be cascading -losses. We may still be able to establish a bound on the losses and to -prove that other protocol runs function -correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow -the strategy illustrated above, but the subgoals can -be much bigger and there are more of them. -\index{protocols!security|)} - -\endinput +\input{Protocol/document/Message} +\input{Protocol/document/Event} +\input{Protocol/document/Public} +\input{Protocol/document/NS_Public}