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 |
| DOIs | |
| Publication status | Published - 2010 |
| Event | 17th ACM Conference on Computer and Communications Security - Chicago, United States Duration: 4 Oct 2010 → 8 Oct 2010 Conference number: 17 |
Conference
| Conference | 17th ACM Conference on Computer and Communications Security |
|---|---|
| Number | 17 |
| Country/Territory | United States |
| City | Chicago |
| Period | 04/10/2010 → 08/10/2010 |
Keywords
- Automated verification, abstract interpretation, revocation, web services, APIs