Stéphanie Delaune, Mark D. Ryan, and Ben Smyth. Automatic verification of privacy properties in the applied pi-calculus. In Proceedings of the 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08), pp. 263–278, IFIP Conference Proceedings 263, Springer, Trondheim, Norway, June 2008.
We develop a formal method verification technique for cryptographic protocols. We focus on proving observational equivalences of the kind \(P \sim 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.
@inproceedings{DRS-ifiptm08,
abstract = {We develop a formal method verification technique for
cryptographic protocols. We~focus on proving
observational equivalences of the kind \(P \sim 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.\par We
demonstrate the practicality of our work with two
case studies.},
address = {Trondheim, Norway},
author = {Delaune, St{\'e}phanie and Ryan, Mark D. and
Smyth, Ben},
booktitle = {{P}roceedings of the 2nd {J}oint i{T}rust and {PST}
{C}onferences on {P}rivacy, {T}rust {M}anagement and
{S}ecurity (IFIPTM'08)},
editor = {Karabulut, Yuecel and Mitchell, John and
Herrmann, Peter and Jensen, Christian Damsgaard},
month = jun,
pages = {263-278},
publisher = {Springer},
series = {IFIP Conference Proceedings},
title = {Automatic verification of privacy properties in the
applied pi-calculus},
volume = {263},
year = {2008},
acceptrate = {22/62},
acronym = {IFIPTM'08},
nmonth = {6},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}