Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases

Sebastian Alexander Mödersheim

Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases

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

247 Downloads (Pure)

Abstract

The abstraction and over-approximation of protocols and web services by a set of Horn clauses is a very successful method in practice. It has however limitations for protocols and web services that are based on databases of keys, contracts, or even access rights, where revocation is possible, so that the set of true facts does not monotonically grow with the transitions. We extend the scope of these over-approximation methods by defining a new way of abstraction that can handle such databases, and we formally prove that the abstraction is sound. We realize a translator from a convenient specification language to standard Horn clauses and use the verifier ProVerif and the theorem prover SPASS to solve them. We show by a number of examples that this approach is practically feasible for wide variety of verification problems of security protocols and web services.

Original language	English
Title of host publication	Proceedings of the 17th ACM Conference on Computer and Communications Security
Number of pages	9
Place of Publication	New York
Publisher	Association for Computing Machinery
Publication date	2010
Pages	351-360
ISBN (Print)	978-1-4503-0244-9
Publication status	Published - 2010
Event	ACM Conference on Computer and Communications Security - Chicago, USA Duration: 1 Jan 2010 → … Conference number: 17

Conference

Conference	ACM Conference on Computer and Communications Security
Number	17
City	Chicago, USA
Period	01/01/2010 → …

Keywords

Automated verification, abstract interpretation, revocation, web services, APIs

Access to Document

SetabstractionFinal published version, 370 KB

http://domino.research.ibm.com/library/cyberdig.nsf/1e4115aea78b6e7c85256b360066f0d4/bb9cc6dc17a3bb3285257718003f57f4!OpenDocument

Cite this

Mödersheim, S. A. (2010). Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases. In Proceedings of the 17th ACM Conference on Computer and Communications Security (pp. 351-360). Association for Computing Machinery. http://domino.research.ibm.com/library/cyberdig.nsf/1e4115aea78b6e7c85256b360066f0d4/bb9cc6dc17a3bb3285257718003f57f4!OpenDocument

@inproceedings{621a880ab75b411d9f71a69056ca7126,

title = "Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases",

abstract = "The abstraction and over-approximation of protocols and web services by a set of Horn clauses is a very successful method in practice. It has however limitations for protocols and web services that are based on databases of keys, contracts, or even access rights, where revocation is possible, so that the set of true facts does not monotonically grow with the transitions. We extend the scope of these over-approximation methods by defining a new way of abstraction that can handle such databases, and we formally prove that the abstraction is sound. We realize a translator from a convenient specification language to standard Horn clauses and use the verifier ProVerif and the theorem prover SPASS to solve them. We show by a number of examples that this approach is practically feasible for wide variety of verification problems of security protocols and web services.",

keywords = "Automated verification, abstract interpretation, revocation, web services, APIs",

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

year = "2010",

language = "English",

isbn = "978-1-4503-0244-9",

pages = "351--360",

booktitle = "Proceedings of the 17th ACM Conference on Computer and Communications Security",

publisher = "Association for Computing Machinery",

address = "United States",

note = "ACM Conference on Computer and Communications Security, CCS 2010 ; Conference date: 01-01-2010",

}

Mödersheim, SA 2010, Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases. in Proceedings of the 17th ACM Conference on Computer and Communications Security. Association for Computing Machinery, New York, pp. 351-360, ACM Conference on Computer and Communications Security, Chicago, USA, 01/01/2010. <http://domino.research.ibm.com/library/cyberdig.nsf/1e4115aea78b6e7c85256b360066f0d4/bb9cc6dc17a3bb3285257718003f57f4!OpenDocument>

Abstraction by Set-Membership : Verifying Security Protocols and Web Services with Databases. / Mödersheim, Sebastian Alexander.

Proceedings of the 17th ACM Conference on Computer and Communications Security. New York : Association for Computing Machinery, 2010. p. 351-360.

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

TY - GEN

T1 - Abstraction by Set-Membership

T2 - ACM Conference on Computer and Communications Security

AU - Mödersheim, Sebastian Alexander

N1 - Conference code: 17

PY - 2010

Y1 - 2010

N2 - The abstraction and over-approximation of protocols and web services by a set of Horn clauses is a very successful method in practice. It has however limitations for protocols and web services that are based on databases of keys, contracts, or even access rights, where revocation is possible, so that the set of true facts does not monotonically grow with the transitions. We extend the scope of these over-approximation methods by defining a new way of abstraction that can handle such databases, and we formally prove that the abstraction is sound. We realize a translator from a convenient specification language to standard Horn clauses and use the verifier ProVerif and the theorem prover SPASS to solve them. We show by a number of examples that this approach is practically feasible for wide variety of verification problems of security protocols and web services.

AB - The abstraction and over-approximation of protocols and web services by a set of Horn clauses is a very successful method in practice. It has however limitations for protocols and web services that are based on databases of keys, contracts, or even access rights, where revocation is possible, so that the set of true facts does not monotonically grow with the transitions. We extend the scope of these over-approximation methods by defining a new way of abstraction that can handle such databases, and we formally prove that the abstraction is sound. We realize a translator from a convenient specification language to standard Horn clauses and use the verifier ProVerif and the theorem prover SPASS to solve them. We show by a number of examples that this approach is practically feasible for wide variety of verification problems of security protocols and web services.

KW - Automated verification, abstract interpretation, revocation, web services, APIs

M3 - Article in proceedings

SN - 978-1-4503-0244-9

SP - 351

EP - 360

BT - Proceedings of the 17th ACM Conference on Computer and Communications Security

PB - Association for Computing Machinery

CY - New York

Y2 - 1 January 2010

ER -