key: 2011-Applied-pi-calculus
type: incollection
title: Applied pi calculus
authors:
  - Mark D. Ryan
  - Ben Smyth
editors:
  - Véronique Cortier
  - Steve Kremer
year: 2011
month: 3
booktitle: Formal Models and Techniques for Analyzing Security Protocols
chapter: "6"
publisher: IOS Press
doi: 10.3233/978-1-60750-714-7-112
image: /img/pubs-formal-methods-and-techniques-for-analyzing-security-protocols.jpg
description: >-
  The applied pi calculus is a language for modelling security protocols. In this book chapter we
  present the applied pi calculus in a tutorial style.
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.
links:
  - file: Smyth10-applied-pi-calculus.pdf
    text: Extended version
  - label: Buy
    items:
      - url: >-
          http://www.amazon.co.uk/Techniques-Analyzing-Protocols-Cryptology-Information/dp/1607507137/
        text: Amazon.co.uk
      - url: http://www.amazon.com/Formal-Techniques-Analyzing-Security-Protocols/dp/1607507137/
        text: Amazon.com
      - url: http://www.iospress.nl/book/formal-models-and-techniques-for-analyzing-security-protocols/
        text: IOS
  - url: https://doi.org/10.3233/978-1-60750-714-7-112
    text: Official version