Iterative Horn Solver

This is a historic web page. Unfortunately, several links no longer function. They will not be updated, I apologise. However, the code can still be downloaded below.

This is the webpage for the Iterative Horn Solver: a tool for solving arbitrary Horn formulas. In the general case of Horn formulas outside the class H1 it returns an approximate solution, but it iteratively refines the Horn formula, allowing it to precisely solve many formulas outside of H1.

The solver is an implementation of the Horn solver and the iterative scheme described in Christoffer Rosenkilde Nielsen's Ph.D. thesis "A Verifiable Language for Cryptographic Protocols", DTU 2008. The thesis can be found here.

The solver has an end-user interface, usable for someone who wishes to solve Horn formulas and manually interpret the output. The backend is highly flexible, and can typeset both the results and input Horn formula in ASCII, HTML and LaTeX. The produced HTML are especially very convenient for interpreting the results.

Furthermore, the solver has a well-documented library interface in OCaml. This library includes all functionality of the end-user binary, including solver, parser and output functions. The output functions are very parameterisable, making it possibly to easily output reinterpretations of the Horn formula or result as needed.

A guide for the end-user interface is included in the distribution. A technical guide on the implementation of the solver, including a description of the library interface, is also included. Lastly, the source code has been thoroughly annotated with OCamldoc comments, fully describing the library interface and more. These are pre-generated and distributed with the source code.

The tool was developed as part of an implementation for the CryptoKlaim Analyser, also described in the aforementioned Ph.D. thesis. The homepage for that project can be found here

Please report bugs and suggestions for improvements to "jsrn at jsrn . dk". I hope the tool will be useful for you.

Johan Sebastian Rosenkilde Nielsen

Download (version )

The solver is written in OCaml and is as such platform independent, running on any platform with an OCaml interpreter. It can be downloaded here for various platforms. Compiling the solver to native-code greatly improves speed, so if you are solving large formulas, this is recommended. It is distributed as free software under the GPL license, version 3 or later.

The version numbering is simply the version control revision, and does not follow any release system. The changelog (version control dump) for the solver can be found here.

Byte-code (all platforms)

     Full distribution (binary, library, source and documentation)

     Compiled distribution (binary, library and documentation)

Source (all platforms)

     Full distribution (source and documentation)

Native-code (only linux-amd64)

     Full distribution (binary, library, source and documentation)

     Compiled distribution (binary, library and documentation)

Last updated at Thu Nov 27 16:39:54 CET 2014.