ITU

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

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-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 JournalConference articleResearchpeer-review

Harvard

APA

Vancouver

Author

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