tamarin’s language and algorithms for constructing proofs build on research in both term rewriting and order-sorted equational logic. Our focus in this book is however practically oriented: using Tamarin to reason about security protocols rather than explaining this underlying theory. Nevertheless, some knowledge of these foundations is helpful for specifying protocols and understanding how to interact with tamarin. General background on these topics may be found in the book on term rewriting by [6] and the survey on order-sorted logic and computation by [104].