Temporary Research Position / Security and Confidentiality

This position is in the frame the PEPR SVP, a collaborative project between IRISA (team Spicy), Inria Paris (team Prosecco), Inria Sophia (team Splits), LORIA (team Pesto), and ENS Paris-Saclay (formal methods laboratory).

This position includes travel to conferences, in particular to present research papers, and visits to Vincent Cheval at Oxford University, with whom we collaborate on this research topic. Travel costs will be covered by PEPR SVP.

The recruited person will study distance bounding protocols, cryptographic protocols that allow one participant (verifier) to ensure that another participant (prover) is at most at distance d from him, by measuring the travel time of exchanged messages and using the fact that messages travel at most the speed of light. In many of these protocols, the prover sends a challenge to the verifier, who responds with a 0 or 1 bit. If the prover wants to cheat on his distance, he will have to answer randomly before receiving the verifier's challenge, and therefore normally has a probability 1/2 of answering correctly. This operation is repeated several times, so that the probability of success is very small. More precisely, the recruited person will work on a type of attack known as “white box”, which enables the prover to answer before receiving the verifier's challenge, while still having a probability of success greater than 1/2.

Although these attacks have been shown to have negative effects on several protocols in the literature, they remain little explored: only two protocols, out of more than twenty, have been the subject of in-depth analysis [1]. This analysis is intrinsically probabilistic, complex and often requires error-prone ad hoc methods. For example, the security analysis of the Hancke and Kuhn protocol was incorrectly estimated in [1] and corrected in [2]. Moreover, manual proofs are often limited to a restricted set of attack strategies, leaving open the possibility that more effective strategies exist. This is the case in Munilla and Peinado's protocol analysis [3], where a more optimal attack strategy was neglected in [1]. The goal of this project is to provide an extensive study of such white-box attacks on distance bounding protocols.

Bibliographic references

[1] G. Avoine, M. A. Bingöl, S. Kardas, C. Lauradoux, and B. Martin.
A framework for analyzing RFID distance bounding protocols.
J. Comput. Secur., 19(2):289--317, 2011.

[2] G. Avoine, M. A. Bingöl, I. Boureanu, S. Capkun, G. P. Hancke, S. Kardas, C. H. Kim, C. Lauradoux, B. Martin, J. Munilla, A. Peinado, K. B. Rasmussen, D. Singelée, A. Tchamkerten, R. Trujillo-Rasua, and S. Vaudenay. Security of Distance-Bounding: A Survey. ACM Comput. Surv., 51(5):94:1--94:33, 2019.

[3] J. Munilla and A. Peinado. Distance bounding protocols for RFID enhanced by using void-challenges and analysis in noisy channels. Wireless Communications and Mobile Computing}, 8(9):1227--1232, 2008.

Collaboration

The recruited person will work with Bruno Blanchet (Inria Paris, team Prosecco) and will also collaborate with Vincent Cheval (Oxford University).

Main activities:

• Perform a complete literature review to enumerate existing distance bounding protocols and see if they are also susceptible to attack.
• For each protocol, recalculate the attacker's probability of mounting the attacks.
• Depending on the type of attack, run simulations on different implementations of hash functions, encryption, etc. to see if our assumptions about the bit distribution of the outputs are correct, and also to estimate the computing time required by the attacker.
• Look at older hash functions (like SHA1 and MD5) that are still used in these protocols (as collision resistance, which is broken for these functions, is not needed in distance bounding protocols) and see if we can exploit the algorithms to get better probabilities for the attacker.

More generally, this work will lead to a theoretical study of the particular security properties of the hashing, encryption and decryption functions on which the security of distance-bounding protocols is based. Ultimately, the aim is to extend the symbolic protocol verification tool ProVerif (https://proverif.inria.fr), so that it can handle this kind of protocol in which security is based on probabilistic arguments.

Technical skills and level required :

 - Strong knowledge in the theory of probabilities

Languages : Fluency in English required

Relational skills : Ability to collaborate with other researchers

Other valued appreciated :

- Knowledge of cryptography, security protocols and formal verification, or ability to learn these topics

• Subsidized meals
• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Social security coverage