FDR2 is a refinement checker for establishing properties of models expressed in CSP. Casper is a program that will take a description of a security protocol in a simple, abstract language, and produce a CSP description of the same protocol, suitable for checking using FDR2. It can be used either to find attacks upon protocols, or to show that no such attack exists, subject to the assumptions of the Dolev-Yao Model (i.e. that the intruder may overhear or intercept messages, decrypt and encrypt messages with keys that he knows, and fake messages, but not perform any cryptological attacks).  

    ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses.

    The CoreASM project focuses on the design of a lean executable ASM (Abstract State Machines) language, in combination with a supporting tool environment for high-level design, experimental validation and formal verification (where appropriate) of abstract system models.

    A symbolic model checker for CTL [latest revision 2.5].

    Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow).
 

    AsmL is an industrial-strength executable specification language. It can be used at any stage of the programming process: design, coding, or testing. It is fully integrated into the Microsoft .NET environment: AsmL models can interoperate with any other .NET assembly, no matter what source language it is written in. AsmL uses XML and Word for literate specifications.

    The Abstract State Machine (ASM) Project (formerly known as the Evolving Algebras Project) was started by Yuri Gurevich as an attempt to bridge the gap between formal models of computation and practical specification methods.
    The ASM thesis is that any algorithm can be modeled at its natural abstraction level by an appropriate ASM. Based upon this thesis, members of the ASM community have sought to develop a methodology based upon mathematics which would allow algorithms to be modeled naturally; that is, described at their natural abstraction levels. The result is a simple methodology for describing simple abstract machines which correspond to algorithms. Plentiful examples exist in the literature of ASMs applied to different types of algorithms.

    AVISPA stands for Automated Validation of Internet Security Protocols and Applications.
    The AVISPA project aims at developing a push-button, industrial-strength technology for the analysis of large-scale Internet security-sensitive protocols and applications.