Formal verification of Cryptographic Protocols

What is a cryptographic protocol?

A cryptographic protocol is a protocol executed by several distant agents through a network where the messages or part of the messages are produced using cryptographic functions (encryption, hashing, etc.). Cryptographic protocols are used for various purpose between the agents:

The mechanism of the protocol is supposed to resist to the attacks of, so called, intruders who are dishonest agents. Verifying a protocol consists in checking that whatever the intruders activity may be they should not be able to modify the expected result of the protocol:

How to achieve formal verification of cryptographic protocols?

The first step towards verification is to model formally, and as precisely as possible, the protocol and the capabilities of the potential intruders. Then, on this formal model, the verification techniques tends either to find some attacks or prove that there is no one. Under some strong restrictions on the model (number of agents, number of protocol sessions, capabilities of the intruder, robustness of cryptographic functions, etc.) and on the protocol (size of the messages, content of the messages) the verification problem can become decidable.

What is the approach of the Lande project for formal verification of cryptographic protocols?

In the Lande project, we chose to do relax as much as possible restrictions on the model in order to remain as close as possible to real problems and protocols. As a consequence, the tackled verification problems are rarely decidable, and the verification techniques are often semi-automatic. Verification of cryptographic protocols require precise and sophisticated analysis techniques in order to guarantee their security under very general verification hypothesis: no limit on the number of runned sessions, no limit on the number of actors running the protocol at the same time. Many works are devoted to attack discovery and generally use model-checking on a bounded model of the protocol. However, when attacks are no longer found, it is necessary to prove than there is no more whatever be the number of sessions to be runned or the number of actors involved in the protocol executions. Several ways to achieve such a proof have already been explored. For instance, it is possible to make the proof by hand or with a proof assistant. However, the proof is generally tedious, not automatic and require a lot of user intuition.

Our approach to cryptographic protocol verification [1] is in between since it is not restricted to a bounded number of sessions, it is not devoted to a specific property to prove, and it is semi-automatic. We apply reachability analysis over term rewriting systems to the verification of cryptographic protocols. Reachability analysis on Term Rewriting Systems is a general purpose verification technique over infinite state systems or programs modeled using Term Rewriting Systems. This technique is implemented in the Timbuk tool. In the case of cryptographic protocol, we encode protocols and intruder capabilities into term rewriting systems and construct an over-approximation of the set of reachable terms. Then, in this over-approximation, if there is no term representing a violation of one of the security property then the protocol is secure. On these aspects, we have successfully applied reachability analysis to the verification of the "view-only'' protocol of the SmartRight digital rights management system developped by Thomson-Multimedia [2].

Note that, this approach and the Timbuk tool is also used by some other research groups to achieve cryptographic protocol verification, like Pierre-Cyrille Heam, Yohan Boichut and Olga Kouchnarenko of the Cassis INRIA project. In this case, Timbuk is used as a verification back-end for the TA4SP protocol verification tool where protocols are defined in HLPSL format (High Level Protocol Specification).
Tools we develop


Our publications on cryptographic protocol verification


[1] (gzipped or not)
T. Genet and F. Klay. Rewriting for Cryptographic Protocol Verification. In Proceedings 17th International Conference on Automated Deduction, Pittsburgh (Pen., USA), volume 1831 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2000.

[2] (gzipped)
T. Genet, Y.-M. Tang-Talpin, and V. Viet Triem Tong. Verification of copy-protection cryptographic protocol using approximations of term rewriting systems. In Proc. of WITS'03, Workshop on Issues in the Theory of Security, 2003.

[3] (pdf)
Y. Boichut, T. Genet, Y. Glouche and O. Heen. Using Animation to Improve Formal Specifications of Security Protocols. In Proceedings of SAR-SSI'07, 2007.