The zero-knowledge type-checker is a tool for automatically analyzing the security of protocols that use zero-knowledge proofs. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. The type-checker relies on the SPASS (or E) automated theorem prover to discharge proof obligations. It is released under the terms of the Apache License.
This release of the zero-knowledge type-checker adds support for security despite compromise and fixes many of the issues in the initial release (release notes). You can grab it from the page of the project.