Combined CPV-TLV Security Protocol Verifier
Several security protocol verifiers were created in order to verify the secrecy and authenticity of security protocols.
A recent one created by Bruno Blanchet - “Cryptographic Protocol Verifier” (CPV), uses Horn clauses. CPV has some important advantages such as being able to determine that a protocol is secure, the ability to handle an unbounded number of sessions of the protocol, and it being reasonably fast. Some of its weaker points are that in some cases a false attack could be identified as truly existing, and that the description of a detected attack is provided as a proof consisting of combinations of Horn clauses and rules which are quite cumbersome.
“Temporal Logic Verifier” (TLV), which provides a flexible environment for the verification of finite state systems, is used as well to verify various properties of security protocols. One of the advantages of TLV with regard to security protocols is that if one knows the nature of a possible attack, TLV can be used to determine easily if this attack indeed exists, and if it does – it presents the attack in a detailed finite state description.
The system presented here, “Combined CPV-TLV”, is developed as a security protocol verifier that joins CPV with TLV, thus gaining the advantages of these two while reducing some of their weaknesses. In the combined system CPV is used to determine that a protocol is secure, and TLV is used to validate or reject attacks which may have been detected by CPV. Therefore, Combined CPV-TLV provides additional and accurate information on the secrecy and authenticity of the protocol under test, over and beyond what CPV and TLV can offer when used separately. As an input, the system accepts a simple description of a protocol and checks it, following Dolev–Yao model.
You can download Combined CPV-TLV and relevant files from here:
Email: arielc at cs.nyu.edu