AIF-ω: Set-Based Protocol Abstraction with Countable Families

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2016

DOI

View graph of relations

Abstraction based approaches like ProVerif are very efficient in protocol verification, but have a limitation in dealing with stateful protocols. A number of extensions have been proposed to allow for a limited amount of state information while not destroying the advantages of the abstraction method. However, the extensions proposed so far can only deal with a finite amount of state information. This can in many cases make it impossible to formulate a verification problem for an unbounded number of agents (and one has to rather specify a fixed set of agents). Our work shows how to overcome this limitation by abstracting state into countable families of sets. We can then formalize a problem with unbounded agents, where each agent maintains its own set of keys. Still, our method does not loose the benefits of the abstraction approach, in particular, it translates a verification problem to a set of first-order Horn clauses that can then be efficiently verified with tools like ProVerif.
Original languageEnglish
Title of host publicationProceedings of the 5th International Conference on Principles of Security and Trust (POST 2016) : Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016)
EditorsFrank Piessens, Luca Viganò
PublisherSpringer
Publication date2016
Pages233-253
ISBN (print)978-3-662-49634-3
ISBN (electronic)978-3-662-49635-0
DOIs
StatePublished - 2016
Event5th International Conference on Principles of Security and Trust - Eindhoven, Netherlands

Conference

Conference5th International Conference on Principles of Security and Trust
Number5
CountryNetherlands
CityEindhoven
Period02/04/201608/04/2016
OtherHeld as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Internet address
SeriesLecture Notes in Computer Science
Volume9635
ISSN0302-9743
CitationsWeb of Science® Times Cited: 0
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

ID: 124244743