Tamarin prover http://www.infsec.ethz.ch/research/software/tamarin Haskell で書かれたセキュリティ・プロトコルの証明器らしい。面白そう。

“The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification of security protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined subterm-convergent rewriting theory.”