ITU

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

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

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
Article number12
Book seriesLecture Notes in Computer Science
Volume9635
Pages (from-to)233-253
Number of pages20
ISSN0302-9743
DOIs
Publication statusPublished - 2 Apr 2016

Downloads

No data available

ID: 81625240