Rewrite

Rewrite is a tree automata completion tool and security protocol analyzer. The current development version can certify its claims through a machine-checkable Coq formal proof.

• rewrite-1.0.tar.bz2 source code (OpenPGP sig)
• rewrite-1.9.0-bin.tar.gz 64-bit binary (development release)
• rewrite-1.9.0-bin-32bit.tar.gz 32-bit binary (development release)
• examples.tar.gz
• tree_automata_examples.tar.gz
• forward.proc forward secrecy example

The archive above includes a brief guide and examples. Rewrite is released under the GNU General Public License.

Rewrite is written in Haskell. The Glasgow Haskell Compiler version 6.4 (or higher compatible) is required to build Rewrite.

Examples

The development version of Rewrite was able to prove the folowing properties. In each case, Rewrite was able to certify its claims with a Coq proof.

• A simple list example (rules,proof)
• A protocol based on Diffie-Hellman (rules,proof)
• The CCA crypto API, used in ATMs (rules,proof)

References

• The completion algorithm used in Rewrite.
• A paper of mine describing the Rewrite protocol analyzer.

Other Tools

• Timbuk tool
• TA4SP Tool
• AVISPA project home page

Software - Home

Roberto Zunino, 2011