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

Sebastian Alexander Mödersheim; Alessandro Bruni

doi:10.1007/978-3-662-49635-0_12

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

Sebastian Alexander Mödersheim, Alessandro Bruni

Department of Applied Mathematics and Computer Science

IT University of Copenhagen

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

1 Downloads (Pure)

Abstract

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 language	English
Title of host publication	Proceedings 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)
Editors	Frank Piessens, Luca Viganò
Publisher	Springer
Publication date	2016
Pages	233-253
ISBN (Print)	978-3-662-49634-3
ISBN (Electronic)	978-3-662-49635-0
DOIs	https://doi.org/10.1007/978-3-662-49635-0_12
Publication status	Published - 2016
Event	5th International Conference on Principles of Security and Trust - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016 Conference number: 5 http://www.etaps.org/index.php/2016/post

Conference

Conference	5th International Conference on Principles of Security and Trust
Number	5
Country/Territory	Netherlands
City	Eindhoven
Period	02/04/2016 → 08/04/2016
Other	Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Internet address	http://www.etaps.org/index.php/2016/post

Series	Lecture Notes in Computer Science
Volume	9635
ISSN	0302-9743

Access to Document

10.1007/978-3-662-49635-0_12

OpenUrl availability

Full text

Cite this

Mödersheim, S. A., & Bruni, A. (2016). AIF-ω: Set-Based Protocol Abstraction with Countable Families. In F. Piessens, & L. Viganò (Eds.), Proceedings 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) (pp. 233-253). Springer. Lecture Notes in Computer Science Vol. 9635 https://doi.org/10.1007/978-3-662-49635-0_12

Mödersheim, Sebastian Alexander ; Bruni, Alessandro. / AIF-ω: Set-Based Protocol Abstraction with Countable Families. Proceedings 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). editor / Frank Piessens ; Luca Viganò. Springer, 2016. pp. 233-253 (Lecture Notes in Computer Science, Vol. 9635).

@inproceedings{c24c58c8359f495f9fe0210a2da2bf11,

title = "AIF-ω: Set-Based Protocol Abstraction with Countable Families",

abstract = "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.",

author = "M{\"o}dersheim, {Sebastian Alexander} and Alessandro Bruni",

year = "2016",

doi = "10.1007/978-3-662-49635-0_12",

language = "English",

isbn = "978-3-662-49634-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "233--253",

editor = "Piessens, {Frank } and Vigan{\`o}, {Luca }",

booktitle = "Proceedings of the 5th International Conference on Principles of Security and Trust (POST 2016)",

note = "5th International Conference on Principles of Security and Trust, POST/ETAPS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",

url = "http://www.etaps.org/index.php/2016/post",

}

Mödersheim, SA & Bruni, A 2016, AIF-ω: Set-Based Protocol Abstraction with Countable Families. in F Piessens & L Viganò (eds), Proceedings 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). Springer, Lecture Notes in Computer Science, vol. 9635, pp. 233-253, 5th International Conference on Principles of Security and Trust, Eindhoven, Netherlands, 02/04/2016. https://doi.org/10.1007/978-3-662-49635-0_12

AIF-ω: Set-Based Protocol Abstraction with Countable Families. / Mödersheim, Sebastian Alexander; Bruni, Alessandro.
Proceedings 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). ed. / Frank Piessens; Luca Viganò. Springer, 2016. p. 233-253 (Lecture Notes in Computer Science, Vol. 9635).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

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

AU - Mödersheim, Sebastian Alexander

AU - Bruni, Alessandro

N1 - Conference code: 5

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-49635-0_12

DO - 10.1007/978-3-662-49635-0_12

M3 - Article in proceedings

SN - 978-3-662-49634-3

T3 - Lecture Notes in Computer Science

SP - 233

EP - 253

BT - Proceedings of the 5th International Conference on Principles of Security and Trust (POST 2016)

A2 - Piessens, Frank

A2 - Viganò, Luca

PB - Springer

T2 - 5th International Conference on Principles of Security and Trust

Y2 - 2 April 2016 through 8 April 2016

ER -

Mödersheim SA, Bruni A. AIF-ω: Set-Based Protocol Abstraction with Countable Families. In Piessens F, Viganò L, editors, Proceedings 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). Springer. 2016. p. 233-253. (Lecture Notes in Computer Science, Vol. 9635). doi: 10.1007/978-3-662-49635-0_12

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

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this