SafeTLS
2016-2020


                                   

Our Methodology


Protocol analysis can be done at several levels, and using various tools. We choose in particular to use the following methodologies.


Provable Security.

The security-by-design paradigm aims to provide schemes that are secure against generic attacks, as opposed to protocols that resist attacks known up to that point. This paradigm allows experts to prove cryptographic schemes secure before they are deployed in real-world applications.

The greatest strength of provable security is its ability to guarantee security against arbitrary attacks within a generic adversarial category. This includes both existing and future attacks.

However, one of the main limitations of provable security is that a security proof is only as accurate as the model in which it is given. There is a clear tradeoff between the accuracy of the model and the complexity of the proof; to make proofs possible, many details of the system and the adversary’s interactions are abstracted away. Consequently, protocols that are proved secure may still have flaws, as was the case of TLS 1.2.

The existence of these attacks does not contradict the security proof; they simply fall outside the security model. On the other hand, an overly-strong security model usually leads to either impossibility proofs (i.e. a proof tht the desired security notion is unattainable) or to a lack of a proof – which may mean the protocol is insecure, or it may mean that no proof can be formalized.

Provable security remains to date one of the strongest tools permitting sound protocol design for real-world applications. We use this approach too, mitigating some of its deficiencies by one of the following solutions:

  • Better models: We will extend models to include as many details of real-world protocol runs as possible.
  • Automated proofs: Where provable security fails, we will use tools providing automated proofs, such as EasyCrypt.
  • Hybrid models: We will also consider the possibility of hybrid proofs, part of the guarantees being given by automated verification, and the rest, by the more exact provable security methodology.


Automated Proofs.

A promising solution to the shortcomings of provable security is to use the automated verification of cryptographic systems. Although many such frameworks exist for the symbolic model of cryptography, comparatively little work has been done to develop machine-checked frameworks to reason directly in the computational model commonly used by cryptographers.

EasyCrypt is an automated tool proposed by Barthe et al. for checking cryptographic proof using formal methods. It implements a probabilistic Hoare logic pHL for bounding the probability of post-conditions, and embeds pRHL and pHL into an ambient logic that can for instance be used to perform hybrid arguments. A proof of security of authenticated key-exchange has already been done in EasyCrypt and proofs have been derived for the NAXOS and NETS protocols.

An extension to this tool allows the use of the CompCert compiler, towards generating assembly code that is secure, in particular against side-channel attacks.


© 2017 Univ. Rennes 1
Last modified on 22/06/2017