Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Proving More Observational Equivalences with ProVerif
verfasst von : Vincent Cheval, Bruno Blanchet
Erschienen in: Principles of Security and Trust
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.