fix: refined language around source lemmas

Author: dmzimmerman

languages/tamarin.tex

@@ -295,15 +295,15 @@ \subsubsection{Lemmas}
 
 Tamarin lemmas are divided into two main types: \emph{source} lemmas and ``regular'' lemmas. Our suggested guidelines for writing these differ slightly, because of the different ways that Tamarin uses them.
 
-Tamarin uses source lemmas to help identify the possible sources of certain messages. It starts the verification process by identifying all the possible sources for input messages to each rule, so that it can reason modularly about the rule's behavior. However, in some cases it is not able to do that identification automatically and requires ``hints''; when this occurs, Tamarin reports that there are ``partial deconstructions left'' after source refinement. 
+Tamarin uses source lemmas to help identify the possible sources of certain messages. It starts the verification process by identifying all the possible sources for input messages to each rule, so that it can reason modularly about every rule's behavior. However, in some cases it is not able to do that identification automatically and requires ``hints''; when this occurs, Tamarin reports that there are ``partial deconstructions left'' after source refinement. 
 
 These hints take the form of lemmas that, roughly, state ``if some action fact $Y$ related to a specific message $m$ occurs in the trace, either another action fact $X$ related to $m$ occurred previously in the trace, or the adversary previously derived $m$ (or some necessary component of $m$) on its own.'' Generally, $Y$ is an action fact that corresponds to the reception of $m$, and $X$ is an action fact that corresponds to the creation and sending of $m$. The canonical example of this occurs when $m$ contains a nonce; the source lemma allows Tamarin to connect the creation of the fresh nonce by some rule (or SAPIC+ statement) with the reception of that nonce by another rule (or SAPIC+ statement). 
 
-When you tell Tamarin to prove all the lemmas in a theory (e.g., when executing ``\texttt{tamarin-prover -{}-prove theory.spthy}'' on the command line), it will first prove the source lemmas, then reuse them as restrictions when refining the sources of messages and proving the remaining lemmas. However, when using Tamarin to prove one or more lemmas in a theory selectively (or interactively), Tamarin simply \emph{assumes} that all the source lemmas are valid. It is therefore critical to ensure that the source lemmas are actually valid by explicitly having Tamarin prove them, as they can otherwise cause unsoundness.
+When you tell Tamarin to prove all the lemmas in a theory (e.g., when executing ``\texttt{tamarin-prover -{}-prove theory.spthy}'' on the command line), it will first prove the source lemmas inductively using the raw sources, then use them to refine the sources, and finally prove the remaining lemmas using the refined sources. However, when using Tamarin to prove one or more lemmas in a theory selectively (or interactively), Tamarin simply \emph{assumes} that all the source lemmas are valid, uses them to refine the sources, and proves the lemmas using the refined sources. It is therefore critical to ensure that the source lemmas are \emph{actually} valid by explicitly having Tamarin prove them, as they can otherwise cause unsoundness.
 
 Source lemmas almost always take the form seen above in lemma \lstinline{Sources}: a conjunction of universal quantifiers, each of which constrains every occurrence of an ``input'' action fact (in the first quantifier, \lstinline{IN_INITIATOR_4_Kab(m, n)}) to occur chronologically after either a corresponding adversary knowledge fact (\lstinline{KU(n)}) or ``output'' action fact (\lstinline{OUT_SERVER_4_Kab(m, n)}). While it is possible to provide Tamarin with multiple source lemmas in a single theory, we have found that sometimes Tamarin is unable to automatically prove multiple source lemmas individually even though it is able to prove their conjunction. Therefore, we recommend always writing a single conjunctive source lemma.
 
-With respect to regular lemmas, we recommend keeping them as simple as possible (while, of course, accurately capturing the security properties you want to prove) and building up complex lemmas from simpler ones where possible. When proving lemmas for an entire theory, Tamarin proceeds in the order they appear in the theory; you can write foundational lemmas early in the theory and flag them with Tamarin's \lstinline{[reuse]} attribute so that they will be reused in later proofs. It can also be useful to flag a lemma with \lstinline{[hide_lemma=...]} if you explicitly do \emph{not} want its proof to reuse a particular lemma, and with \lstinline{[use_induction]} if you want Tamarin to start its proof with induction rather than simplification.
+With respect to regular lemmas, we recommend keeping them as simple as possible (while, of course, accurately capturing the security properties you want to prove) and building up complex lemmas from simpler ones where possible. When proving lemmas for an entire theory, Tamarin proceeds in the order they appear in the theory (except that source lemmas are always proven first, regardless of where in the theory they appear); you can therefore write foundational lemmas early in the theory and flag them with Tamarin's \lstinline{[reuse]} attribute so that they will be reused in later proofs. It can also be useful to flag a lemma with \lstinline{[hide_lemma=...]} if you explicitly do \emph{not} want its proof to reuse a particular lemma, and with \lstinline{[use_induction]} if you want Tamarin to start its proof with induction rather than simplification.
 
 The specific security properties you choose to encode in lemmas is, of course, up to you, and highly dependent on the specifics of your Tamarin theory. However, we \emph{strongly} recommend that for each protocol or subprotocol described in your theory, you have \emph{at least} an ``executability'' lemma to demonstrate that non-trivial executions of that protocol or subprotocol are possible, and that you ensure that lemma can be verified.