key: 2008-towards-verification-of-observational-equivalence
type: inproceedings
title: Automatic verification of privacy properties in the applied pi-calculus
authors:
  - Delaune, Stéphanie
  - Ryan, Mark D.
  - Smyth, Ben
year: 2008
month: 6
booktitle: "IFIPTM'08: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security"
series: International Federation for Information Processing (IFIP)
volume: "263"
pages: 263--278
publisher: Springer
doi: 10.1007/978-0-387-09428-1_17
description: >-
  This paper presents an extension to the class of equivalences which ProVerif is able to
  automatically reason with.
keywords: >-
  Formal methods, Verification, Protocols, Cryptography, Equivalences, Security, ProVerif,
  Electronic voting, Trusted Computing
abstract: >-
  We develop a formal method verification technique for cryptographic protocols.We focus on proving
  equivalences of the kind P ~ Q, where the processes P and Q have the same structure and
  differ only in the choice of terms. The calculus of ProVerif, a variant of the applied pi
  calculus, makes some progress in this direction. We expand the scope of ProVerif, to provide
  reasoning about further equivalences. We also provide an extension which allows modelling of
  protocols which require global synchronisation. Finally we develop an algorithm to enable
  automated reasoning. We demonstrate the practicality of our work with two case studies.
supersededby:
  - key: 2017-verifying-observational-equivalence
    text: JCS article
links:
  - file: Smyth08-equivalence.IFIP.pdf
    text: Conference paper
  - file: Smyth08-equivalence.pdf
    text: Technical Report
  - url: https://doi.org/10.1007/978-0-387-09428-1_17
    text: Official version