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 using one of the following methods (also detailed below): automated verification, cryptanalysis, and side-channel analysis.
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.
Throughout the last decades several tools for automated verification have been designed, e.g., Proverif, Scyther,Tamarin, Avispa. Each tool has its own approach to verifying cryptographic protocols, and they leverage the significant computational power of a computer to run much larger-scales analyses than could be done by hand. Such tools can be used to find flaws in cryptographic designs, but also to prove them secure. An aspect we take into account is the large-scale analysis of both users and data. Depending on the protocols we will design throughout this project, the most appropriate automated-verification tool will be deployed towards obtaining a formal proof of their security. We will also use such tools to find any existing flaws in current designs, or identifying weak spots in the complex 5G infrastructure.
Cryptanalysis
Security proofs -- whether automated or computational -- can provide generic and formal guarnatees regarding the properties of cryptographic primitives and protocols. However, two of their main limitations are: the inability to take into account all the details of real-world attacks; and the necessity of basing the proof on some assumptions regarding the security of underlying primitives. Indeed, some primitives, such as hash functions and block- and stream-ciphers, can only be provided with limited security proofs. Consequently the security both of those primitives themselves and all cryptographic countermeasures using them rely on an assumption, rather than a proof of their security. The validity of such assumptions cannot currently be proved; instead we validate such assumptions by subjecting these primitives to extensive cryptanalysis. In other words, one tries to find ways to attack such cryptographic algorithms by exploiting their underlying structure.
We want to study the security of lightweight block-ciphers, such as MIDORI, which has been designed to be energy-friendly. It is a variant of AES where the costly operations, such as MixColumn, is replaced by some additions, and the Sbox is also changed using smaller versions. This variant presents some weaknesses from a security point-of-view since the diffusion is not as efficient as in AES, but the higher number of rounds of MIDORI makes this variant secure (even though a weakness in the constants has been pointed out using an invariant subspace attack). We also want to study such framework more deeply and it would be interesting to study a variant of AES where the key-schedule will be less costly in term of Sbox and in particular if it is linear. Such variants have been proposed but their security have been poorly investigated so far.
Side-channel analysis.
Although provable security may give an indication about the soundness of an algorithm, it cannot automatically guarantee the security of implementations of that algorithm. The latter will still be subject to so-called side-channel analysis, which uses physical characteristics of devices and the implementation of various cryptographic primitives in order to learn something about the secrets they are hiding -- including plaintexts, keys, etc.
Most of the devices in a 5G network could be subject to side-channel attacks. Indeed, an attacker will have a physical access to stolen or lost personal devices and to a variety of small connected devices as surveillance cameras for instance. Moreover, the adversary may be able to make her own software run on smart devices (e.g. mobile app). Thus, the cryptographic primitives and protocols used should also be studied with regard to this specific kind of threats. In this project, we will look for new side-channel attacks on those algorithms and their potential mitigation. In order to assess the relevancy of those attacks (and the corresponding countermeasures), their impact in the particular context of 5G networks will be considered and experiments on representative hardware will be conducted.