Automatic verification of privacy properties in the applied pi-calculus

Delaune, Stéphanie, Ryan, Mark D. & Smyth, Ben (2008) Automatic verification of privacy properties in the applied pi-calculus. In IFIPTM'08: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (International Federation for Information Processing (IFIP)), 263–278, Springer.

Download

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.

Bibtex Entry

@inproceedings{2008-towards-verification-of-observational-equivalence,
  author = {Delaune, Stéphanie and Ryan, Mark D. and Smyth, Ben},
  title = {{Automatic verification of privacy properties in the applied pi-calculus}},
  booktitle = {IFIPTM'08: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security},
  year = {2008},
  month = {June},
  volume = {263},
  pages = {263--278},
  series = {International Federation for Information Processing (IFIP)},
  publisher = {Springer},
  doi = {10.1007/978-0-387-09428-1\_17}
}