*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.

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)

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

Roberto Zunino, 2011