ITU

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

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Standard

AIF-ω: Set-Based Protocol Abstraction with Countable Families. / Mödersheim, Sebastian Alexander; Bruni, Alessandro.

In: Lecture Notes in Computer Science, Vol. 9635, 12, 02.04.2016, p. 233-253.

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Harvard

Mödersheim, SA & Bruni, A 2016, 'AIF-ω: Set-Based Protocol Abstraction with Countable Families', Lecture Notes in Computer Science, vol. 9635, 12, pp. 233-253. https://doi.org/10.1007/978-3-662-49635-0_12

APA

Mödersheim, S. A., & Bruni, A. (2016). AIF-ω: Set-Based Protocol Abstraction with Countable Families. Lecture Notes in Computer Science, 9635, 233-253. [12]. https://doi.org/10.1007/978-3-662-49635-0_12

Vancouver

Mödersheim SA, Bruni A. AIF-ω: Set-Based Protocol Abstraction with Countable Families. Lecture Notes in Computer Science. 2016 Apr 2;9635:233-253. 12. https://doi.org/10.1007/978-3-662-49635-0_12

Author

Mödersheim, Sebastian Alexander ; Bruni, Alessandro. / AIF-ω: Set-Based Protocol Abstraction with Countable Families. In: Lecture Notes in Computer Science. 2016 ; Vol. 9635. pp. 233-253.

Bibtex

@inproceedings{4f436fe20c8b4adb91273f5c00cf76ea,
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",
month = apr,
day = "2",
doi = "10.1007/978-3-662-49635-0_12",
language = "English",
volume = "9635",
pages = "233--253",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer",

}

RIS

TY - GEN

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

AU - Mödersheim, Sebastian Alexander

AU - Bruni, Alessandro

PY - 2016/4/2

Y1 - 2016/4/2

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 - Conference article

VL - 9635

SP - 233

EP - 253

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

M1 - 12

ER -

ID: 81625240