4个协议验证工具

Scyther
Scyther is a state-of-the-art tool for the automatic verification of security protocols.


mCRL toolset
µCRL (micro CRL - written as mCRL if the symbol µ is not available) is a process algebraic language that was especially developed to take account of data in the study of communicating processes. It is basically intended to study description and analysis techniques for (large) distributed systems.


mCRL2
mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.


CADP
CADP ("Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package") is a toolbox for the design of communication protocols and distributed systems.