Conference paper · Book chapter
AIF-ω: Set-Based Protocol Abstraction with Countable Families
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2016 |
| Pages: | 233-253 |
| Proceedings: | 5th International Conference on Principles of Security and TrustInternational Conference on Principles of Security and Trust |
| Series: | Lecture Notes in Computer Science |
| Journal subtitle: | Held As Part of the European Joint Conferences on Theory and Practice of Software (etaps 2016) |
| ISBN: | 3662496348 , 3662496356 , 9783662496343 and 9783662496350 |
| ISSN: | 03029743 and 16113349 |
| Types: | Conference paper and Book chapter |
| DOI: | 10.1007/978-3-662-49635-0_12 |
| ORCIDs: | Mödersheim, Sebastian Alexander |
