Set-Pi: Set Membership pi-Calculus

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedings – Annual report year: 2015Researchpeer-review

Documents

DOI

View graph of relations

Communication protocols often rely on stateful mechanisms to ensure certain security properties. For example, counters and timestamps can be used to ensure authentication, or the security of communication can depend on whether a particular key is registered to a server or it has been revoked. ProVerif, like other state of the art tools for protocol analysis, achieves good performance by converting a formal protocol specification into a set of Horn clauses, that represent a monotonically growing set of facts that a Dolev-Yao attacker can derive from the system. Since this set of facts is not state-dependent, the category of protocols of our interest cannot be precisely analysed by such tools, as they would report false attacks due to the over-approximation.

In this paper we present Set-π, an extension of the Applied π-calculus that includes primitives for handling databases of objects, and propose a translation from Set-π into Horn clauses that employs the set-membership abstraction to capture the non-monotonicity of the state. Furthermore, we give a characterisation of authentication properties in terms of the set properties in the language, and prove the correctness of our approach. Finally we showcase our method with three examples, a simple authentication protocol based on counters, a key registration protocol, and a model of the Yubikey security device.
Original languageEnglish
Title of host publicationProceedings of the 28th IEEE Computer Security Foundations Symposium (CSF 2015)
PublisherIEEE
Publication date2015
Pages185-198
ISBN (Print)978-1-4673-7538-2
DOIs
Publication statusPublished - 2015
Event28th IEEE Computer Security Foundations Symposium (CSF 2015) - Verona, Italy
Duration: 13 Jul 201517 Jul 2015
Conference number: 28
http://csf2015.di.univr.it/

Conference

Conference28th IEEE Computer Security Foundations Symposium (CSF 2015)
Number28
CountryItaly
CityVerona
Period13/07/201517/07/2015
Internet address
SeriesI E E E Computer Security Foundations Symposium. Proceedings
ISSN1940-1434
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 117321034