Proving More Observational Equivalences with ProVerif (bibtex)
by Vincent Cheval, Bruno Blanchet
Abstract:
This paper presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. ProVerif can prove observational equivalence between processes that have the same structure but differ by the messages they contain. In order to extend the class of equivalences that ProVerif handles, we extend the language of terms by defining more functions (destructors) by rewrite rules. In particular, we allow rewrite rules with inequalities as side-conditions, so that we can express tests ``if then else'' inside terms. Finally, we provide an automatic procedure that translates a process into an equivalent process that performs as many actions as possible inside terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to automatically prove anonymity in the private authentication protocol by Abadi and Fournet.
Reference:
Proving More Observational Equivalences with ProVerif (Vincent Cheval, Bruno Blanchet), In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013.
Bibtex Entry:
@string{lncs="Lecture Notes on Computer Science"}
@string{spv="Springer Verlag"}
@InProceedings{ChevalBlanchet12,
  author = 	 {Vincent Cheval and Bruno Blanchet},
  title = 	 {Proving More Observational Equivalences with {P}ro{V}erif},
  booktitle = {2nd Conference on Principles of Security and Trust (POST 2013)},
  pages = 	 {226--246},
  year = 	 2013,
  editor = 	 {David Basin and John Mitchell},
  volume = 	 7796,
  series = 	 lncs,
  address = 	 {Rome, Italy},
  month = 	 mar,
  publisher = spv,
  abstract = {This paper presents an extension of the automatic protocol verifier
ProVerif in order to prove more observational equivalences. ProVerif
can prove observational equivalence between processes that have the
same structure but differ by the messages they contain.  In order to
extend the class of equivalences that ProVerif handles, we extend the
language of terms by defining more functions (destructors) by rewrite
rules. In particular, we allow rewrite rules with inequalities as
side-conditions, so that we can express tests ``if then else'' inside
terms.  Finally, we provide an automatic procedure that translates a
process into an equivalent process that performs as many actions as
possible inside terms, to allow ProVerif to prove the desired
equivalence. These extensions have been implemented in ProVerif and
allow us to automatically prove anonymity in the private
authentication protocol by Abadi and Fournet.},
  x-language = {EN},
  x-audience = {international},
  x-town = {Rome},
  x-country = {IT},
  url = {http://prosecco.gforge.inria.fr/personal/bblanche/publications/ChevalBlanchetPOST13.html}
}
Powered by bibtexbrowser