LaTeX code is now generated directly from theory files.
--- 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 \<in> bad"
- Server_not_bad [iff] : "Server \<notin> bad"
+text{*Spy has access to his own key for spoof messages, but Server is secure*}
+specification (bad)
+ Spy_in_bad [iff]: "Spy \<in> bad"
+ Server_not_bad [iff]: "Server \<notin> 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} \<union> used evs
| Gets A X => used evs
- | Notes A X => parts {X} Un (used evs))"
+ | Notes A X => parts {X} \<union> 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 \<in> set evs --> X \<in> used evs"
+apply (induct_tac evs)
+apply (auto split: event.split)
+done
+
+lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> 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} \<union> 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\<in>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 \<subseteq> knows Spy (Says A B X # evs)"
+by (simp add: subset_insertI)
+
+lemma knows_Spy_subset_knows_Spy_Notes:
+ "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
+by force
+
+lemma knows_Spy_subset_knows_Spy_Gets:
+ "knows Spy evs \<subseteq> 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 \<in> set evs --> X \<in> 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 \<in> set evs --> A: bad --> X \<in> 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 \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
+by simp
+
+
+lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
+by (simp add: subset_insertI)
+
+lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
+by (simp add: subset_insertI)
+
+lemma knows_subset_knows_Gets: "knows A evs \<subseteq> 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 \<in> set evs --> X \<in> 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 \<in> set evs --> X \<in> 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 \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> 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 \<in> knows A evs; A \<noteq> Spy |] ==> EX B.
+ Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> 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 \<in> knows Spy evs |] ==> EX A B.
+ Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> 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) \<subseteq> 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 \<in> parts (initState B) ==> X \<in> 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} \<union> used evs"
+by simp
+
+lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
+by simp
+
+lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
+by simp
+
+lemma used_nil_subset: "used [] \<subseteq> 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 \<notin> 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 \<notin> 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 \<subseteq> knows A (e # evs)"
+by (induct e, auto simp: knows_Cons)
+
+lemma initState_subset_knows: "initState A \<subseteq> 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 \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |]
+ ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> 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 \<notin> 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 \<notin> 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 \<notin> 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
--- 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 \<union> (B \<union> A) = B \<union> 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. \<exists>X. Crypt K X \<in> 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 \<in> H ==> X \<in> parts H"
@@ -76,75 +111,825 @@
| Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
-(*Monotonicity*)
-lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
+text{*Monotonicity*}
+lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> 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 \<in> Friend`A) = (x:A)"
+by auto
+
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
+by auto
+
+lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> 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 \<union> H') = keysFor H \<union> keysFor H'"
+by (unfold keysFor_def, blast)
+
+lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
+by (unfold keysFor_def, blast)
+
+text{*Monotonicity*}
+lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> 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 \<in> H ==> invKey K \<in> keysFor H"
+by (unfold keysFor_def, blast)
+
+
+subsection{*Inductive relation "parts"*}
+
+lemma MPair_parts:
+ "[| {|X,Y|} \<in> parts H;
+ [| X \<in> parts H; Y \<in> 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 \<subseteq> 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\<in> parts{} ==> P"
+by simp
+
+text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
+lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
+by (erule parts.induct, blast+)
+
+
+subsubsection{*Unions *}
+
+lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
+by (intro Un_least parts_mono Un_upper1 Un_upper2)
+
+lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
+by (intro equalityI parts_Un_subset1 parts_Un_subset2)
+
+lemma parts_insert: "parts (insert X H) = parts {X} \<union> 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} \<union> parts {Y} \<union> parts H"
+apply (simp add: Un_assoc)
+apply (simp add: parts_insert [symmetric])
+done
+
+lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
+by (intro UN_least parts_mono UN_upper)
+
+lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
+apply (rule subsetI)
+apply (erule parts.induct, blast+)
+done
+
+lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>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\<union>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) \<subseteq> parts(insert X H)"
+by (blast intro: parts_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Idempotence and transitivity *}
+
+lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> 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 \<subseteq> parts H) = (G \<subseteq> parts H)"
+apply (rule iffI)
+apply (iprover intro: subset_trans parts_increasing)
+apply (frule parts_mono, simp)
+done
+
+lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
+by (drule parts_mono, blast)
+
+text{*Cut*}
+lemma parts_cut:
+ "[| Y\<in> parts (insert X G); X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
+by (blast intro: parts_trans)
+
+
+lemma parts_cut_eq [simp]: "X\<in> 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: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> 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 \<Rightarrow> msg set"
for H :: "msg set"
where
- Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
- | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
- | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ Inj [intro,simp] : "X \<in> H \<Longrightarrow> X \<in> analz H"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> X \<in> analz H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> Y \<in> analz H"
| Decrypt [dest]:
- "[|Crypt K X \<in> analz H; Key(invKey K) \<in> analz H|] ==> X \<in> analz H"
+ "\<lbrakk>Crypt K X \<in> analz H; Key(invKey K) \<in> analz H\<rbrakk>
+ \<Longrightarrow> X \<in> analz H"
+(*<*)
+text{*Monotonicity; Lemma 1 of Lowe's paper*}
+lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> 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|} \<in> analz H;
+ [| X \<in> analz H; Y \<in> analz H |] ==> P
+ |] ==> P"
+by (blast dest: analz.Fst analz.Snd)
+
+lemma analz_increasing: "H \<subseteq> analz(H)"
+by blast
+
+lemma analz_subset_parts: "analz H \<subseteq> 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) \<union> analz(H) \<subseteq> analz(G \<union> H)"
+by (intro Un_least analz_mono Un_upper1 Un_upper2)
+
+lemma analz_insert: "insert X (analz H) \<subseteq> 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 \<notin> 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) \<notin> 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) \<in> analz H ==>
+ analz (insert (Crypt K X) H) \<subseteq>
+ 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) \<in> analz H ==>
+ insert (Crypt K X) (analz (insert X H)) \<subseteq>
+ 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) \<in> 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) \<in> 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) \<subseteq>
+ 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\<in> analz (analz H) ==> X\<in> 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 \<subseteq> analz H) = (G \<subseteq> analz H)"
+apply (rule iffI)
+apply (iprover intro: subset_trans analz_increasing)
+apply (frule analz_mono, simp)
+done
+
+lemma analz_trans: "[| X\<in> analz G; G \<subseteq> analz H |] ==> X\<in> analz H"
+by (drule analz_mono, blast)
+
+text{*Cut; Lemma 2 of Lowe*}
+lemma analz_cut: "[| Y\<in> analz (insert X H); X\<in> analz H |] ==> Y\<in> 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\<in> 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 \<subseteq> analz G'; analz H \<subseteq> analz H' |]
+ ==> analz (G \<union> H) \<subseteq> analz (G' \<union> 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 \<union> H) = analz (G' \<union> 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:
+ "[| \<forall>X Y. {|X,Y|} \<notin> H; \<forall>X K. Crypt K X \<notin> 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\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
+apply (erule analz.induct)
+apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
+done
+
+lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>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 \<Rightarrow> msg set"
for H :: "msg set"
where
- Inj [intro]: "X \<in> H ==> X \<in> synth H"
- | Agent [intro]: "Agent agt \<in> synth H"
- | Number [intro]: "Number n \<in> synth H"
- | Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
- | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
- | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+ Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> synth H"
+ | Agent [intro]: "Agent agt \<in> synth H"
+ | MPair [intro]:
+ "\<lbrakk>X \<in> synth H; Y \<in> synth H\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> synth H"
+ | Crypt [intro]:
+ "\<lbrakk>X \<in> synth H; Key(K) \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
+(*<*)
+lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> 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 \<in> synth H"
inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
-inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"
inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
-use "Message_lemmas.ML"
+lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> 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 \<union> 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 \<in> synth H"
+
+text {*
+\noindent
+The resulting elimination rule replaces every assumption of the form
+@{term "Nonce n \<in> synth H"} by @{term "Nonce n \<in> 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 \<subseteq> 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) \<union> synth(H) \<subseteq> synth(G \<union> H)"
+by (intro Un_least synth_mono Un_upper1 Un_upper2)
+
+lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
+by (blast intro: synth_mono [THEN [2] rev_subsetD])
+
+subsubsection{*Idempotence and transitivity *}
+
+lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
+by (erule synth.induct, blast+)
+
+lemma synth_idem: "synth (synth H) = synth H"
+by blast
+
+lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> 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\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H"
+by (drule synth_mono, blast)
+
+text{*Cut; Lemma 2 of Lowe*}
+lemma synth_cut: "[| Y\<in> synth (insert X H); X\<in> synth H |] ==> Y\<in> synth H"
+by (erule synth_trans, blast)
+
+lemma Agent_synth [simp]: "Agent A \<in> synth H"
+by blast
+
+lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)"
+by blast
+
+lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
+by blast
+
+lemma Crypt_synth_eq [simp]:
+ "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
+by blast
+
+
+lemma keysFor_synth [simp]:
+ "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
+by (unfold keysFor_def, blast)
+
+
+subsubsection{*Combinations of parts, analz and synth *}
+
+lemma parts_synth [simp]: "parts (synth H) = parts H \<union> 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 \<union> H) = analz (G \<union> 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\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> 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} \<subseteq> synth (analz H) \<union> parts H"} *}
+lemma Fake_parts_insert:
+ "X \<in> synth (analz H) ==>
+ parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
+apply (drule parts_insert_subset_Un)
+apply (simp (no_asm_use))
+apply blast
+done
lemma Fake_parts_insert_in_Un:
"[|Z \<in> parts (insert X H); X: synth (analz H)|]
==> Z \<in> synth (analz H) \<union> parts H";
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
+text{*@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put
+ @{term "G=H"}.*}
+lemma Fake_analz_insert:
+ "X\<in> synth (analz G) ==>
+ analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
+apply (rule subsetI)
+apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> 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 \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
+by (blast intro: analz_subset_parts [THEN subsetD])
+
+lemma analz_disj_parts [simp]:
+ "(X \<in> analz H | X \<in> parts H) = (X \<in> 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|} \<in> synth (analz H)) =
+ (X \<in> synth (analz H) & Y \<in> synth (analz H))"
+by blast
+
+lemma Crypt_synth_analz:
+ "[| Key K \<in> analz H; Key (invKey K) \<in> analz H |]
+ ==> (Crypt K X \<in> synth (analz H)) = (X \<in> 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 \<notin> 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 \<in> parts(insert X H) and Y \<in> 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 \<notin> Key ` A"
+by auto
+
+lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
+by (iprover intro: synth_mono analz_mono)
+
+lemma Fake_analz_eq [simp]:
+ "X \<in> 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 \<in> analz H ==> ALL G. H \<subseteq> 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 \<in> synth (analz H)
+ ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> 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 \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> 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
--- 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: "[] \<in> 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: "\<lbrakk>evs \<in> ns_public; X \<in> synth (analz (knows Spy evs))\<rbrakk>
- \<Longrightarrow> Says Spy B X # evs \<in> ns_public"
- (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (knows Spy evsf))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evsf \<in> ns_public"
+
+
| NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
\<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
# evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
+
| NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
\<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
# evs2 \<in> ns_public"
- (*Alice proves her existence by sending NB back to Bob.*)
+
| NS3: "\<lbrakk>evs3 \<in> ns_public;
Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
\<in> set evs3\<rbrakk>
\<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> 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) \<lbrace>Nonce NA, Agent A\<rbrace>)"}
+may be extended by an event of the form
+@{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"}
+where @{text NB} is a fresh nonce: @{term "Nonce NB \<in> 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 \<notin> 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 \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
-by (erule ns_public.induct, auto)
+ "evs \<in> ns_public
+ \<Longrightarrow> (Key (priK A) \<in> parts (knows Spy evs)) = (A \<in> 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 \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (knows Spy evs)) = (A \<in> 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:
- "\<lbrakk>Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (knows Spy evs);
- Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs);
- evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Nonce NA \<in> analz (knows Spy evs)"
+ "\<lbrakk>Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (knows Spy evs);
+ Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs);
+ evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Nonce NA \<in> 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:
"\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(knows Spy evs);
Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(knows Spy evs);
Nonce NA \<notin> analz (knows Spy evs); evs \<in> ns_public\<rbrakk>
\<Longrightarrow> A=A' \<and> 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]:
+ "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Nonce NB \<notin> 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]:
- "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Nonce NB \<notin> 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 \<in> 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 \<noteq> NAa"} is easy: @{text NB} was
+sent earlier, while @{text NAa} is fresh; formally, we have
+the assumption @{term "Nonce NAa \<notin> 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]:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
Crypt (pubK B) (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow>
Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
by (erule ns_public.induct, auto)
-
+(*>*)
theorem B_trusts_NS3:
- "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
- Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+ "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> 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]:
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
Crypt (pubK B) (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow>
Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> 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(*>*)
--- 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" \<rightleftharpoons> "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 \<notin> symKeys"
+ by (simp add: symKeys_def)
+
+lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
+ by (simp add: symKeys_def)
+
+lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
+ by blast
+
+lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
+ ==> X \<in> 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 \<notin> 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 \<notin> used evs"
+by (rule Nonce_supply_lemma [THEN exE], blast)
+
+lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> 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
--- /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:
--- /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:
--- /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:
--- /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:
--- 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}