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:
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