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

Sebastian Alexander Mödersheim, Alessandro Bruni

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review


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.
BogserieLecture Notes in Computer Science
Sider (fra-til)233-253
Antal sider20
StatusUdgivet - 2 apr. 2016


Dyk ned i forskningsemnerne om 'AIF-ω: Set-Based Protocol Abstraction with Countable Families'. Sammen danner de et unikt fingeraftryk.