@incollection{Smyth11-Applied-pi-calculus,
  author = {Mark D. Ryan and Ben Smyth},
  editor = {Véronique Cortier and Steve Kremer},
  title = {{Applied pi calculus}},
  booktitle = {Formal Models and Techniques for Analyzing Security Protocols},
  year = {2011},
  month = {March},
  chapter = {6},
  publisher = {IOS Press},
  doi = {10.3233/978-1-60750-714-7-112},
  url = {https://publications.bensmyth.com/2011-Applied-pi-calculus/},
  url-pdf = {https://publications.bensmyth.com/files/Smyth10-applied-pi-calculus.pdf},
  url-bib = {https://publications.bensmyth.com/files/Smyth11-Applied-pi-calculus.bib},
  url-yaml = {https://publications.bensmyth.com/files/Smyth11-Applied-pi-calculus.yml},
  url-md = {https://publications.bensmyth.com/files/Smyth10-applied-pi-calculus.md},
  note = {Amazon.co.uk: http://www.amazon.co.uk/Techniques-Analyzing-Protocols-Cryptology-Information/dp/1607507137/; Amazon.com: http://www.amazon.com/Formal-Techniques-Analyzing-Security-Protocols/dp/1607507137/; IOS: http://www.iospress.nl/book/formal-models-and-techniques-for-analyzing-security-protocols/},
  keywords = {cryptographic protocols, security protocols, protocol verification, analyzing, formal methods, formal models, reachability, correspondence properties, observational equivalence, tutorial, Formal Models and Techniques for Analyzing Security Protocols},
  abstract = {The applied pi calculus is a language for modelling security protocols. It is an extension of the pi calculus, a language for studying concurrency and process interaction. This chapter presents the applied pi calculus in a tutorial style. It describes reachability, correspondence, and observational equivalence properties, with examples showing how to model secrecy, authentication, and privacy aspects of protocols.}
}