Iterative Specialisation of Horn Clauses

Christoffer Rosenkilde Nielsen, Flemming Nielson, Hanne Riis Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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 languageEnglish
    Title of host publicationLecture Notes in Computer Science
    VolumeVolume 4960
    PublisherSpringer
    Publication date2008
    Pages131-145
    ISBN (Print)978-3-540-78738-9
    DOIs
    Publication statusPublished - 2008
    Event17th European Symposium on Programming - Budapest, Hungary
    Duration: 1 Jan 2008 → …
    Conference number: 17
    http://esop2008.doc.ic.ac.uk/

    Conference

    Conference17th European Symposium on Programming
    Number17
    Country/TerritoryHungary
    CityBudapest
    Period01/01/2008 → …
    Internet address

    Keywords

    • Horn clauses, Cryptography, Protocols, H1

    Fingerprint

    Dive into the research topics of 'Iterative Specialisation of Horn Clauses'. Together they form a unique fingerprint.

    Cite this