Abstract
We present a generic algorithm for solving Horn clauses through iterative specialisation. The algorithm is generic in the sense that it can be instantiated with any decidable fragment of Horn clauses, resulting in a solution scheme for general Horn clauses that guarantees soundness and termination, and furthermore, it presents sufficient criteria for completeness. We then demonstrate the use of the framework, by creating an instance of it, based on the decidable class ${\mathcal{H}_1}$, capable of solving a non-trivial protocol analysis problem based on the Yahalom protocol.
Original language | English |
---|---|
Title of host publication | Lecture Notes in Computer Science |
Volume | Volume 4960 |
Publisher | Springer |
Publication date | 2008 |
Pages | 131-145 |
ISBN (Print) | 978-3-540-78738-9 |
DOIs | |
Publication status | Published - 2008 |
Event | 17th European Symposium on Programming - Budapest, Hungary Duration: 1 Jan 2008 → … Conference number: 17 http://esop2008.doc.ic.ac.uk/ |
Conference
Conference | 17th European Symposium on Programming |
---|---|
Number | 17 |
Country/Territory | Hungary |
City | Budapest |
Period | 01/01/2008 → … |
Internet address |
Keywords
- Horn clauses, Cryptography, Protocols, H1