How can we ensure that communication technology is flawless? How can we predict all possible attack scenarios? How can the interactions between thousands of users and the resulting vulnerabilities be taken into account? What exactly do we mean by “security”: user anonymity, authentication, the confidentiality of exchanges, the non-traceability of stored data?
Challenges for smartphones, bank cards, online shopping, etc.
At first glance, the sheer number of questions surrounding the security of protocols is enough to make you dizzy. For Itsaka Rakotonirina, however, this is a cause for enthusiasm:“I first became aware of this field of research as part of an internship at Inria Nancy, during my Master’s degree in fundamental computing. I found the level of complexity captivating. It takes years for any progress to be made. However, they have an impact on the use of smartphones, bank cards, online retailers, etc.”
In Nancy, the young PhD student joined the PESTO team, which had laid some of the groundwork in relation to these questions. The researchers divide their work into different security aspects (anonymity, the confidentiality of electronic voting, etc.), which are then evaluated in turn. They avoid becoming lost in scenarios involving thousands of simultaneous users, which are often too difficult to solve through calculation, instead choosing to intentionally reduce the number.“With three participants for electronic voting, or five for biometric passports, we are able to cover the majority of known attacks. These are sometimes highly sophisticated.”
Verifying properties as opposed to testing an infinite number of scenarios
Lastly, the researchers don’t exhaust themselves by endlessly testing different scenarios. They verify that the cryptographic protocols are able to intrinsically guarantee a given property “through construction”, using a mathematical demonstration.
Itsaka Rakotonirina's PhD thesis is on designing and programming an automatic proof generator.“I begin with what we want the protocol to do; non-traceability is guaranteed, for example, if it is impossible to distinguish between the protocol executed by two agents, A and B, and the protocol executed twice by either A or B. I then translate this into mathematical language, before feeding it into the tool that we have programmed in order for analysis of the protocol to be carried out as quickly as possible.”
A quick and comprehensive verification tool
This approach can be applied to all security properties, unlike many verification tools, which specialise in either one or the other. Inria Nancy has deployed it since 2014 in DEEPSEC*, a quick and comprehensive tool.“We make improvements to it on a regular basis”, adds Itsaka.We were recently able to verify the confidentiality of an electronic voting protocol in just a few seconds, something that had previously taken 12 hours.”
It wasn’t long before the young PhD student’s research attracted attention. In the spring of 2018, the paper that he co-wrote with his two supervisors for the international IEEE Symposium on Security and Privacy received a Distinguished Paper Award. In early 2019, Microsoft Research offered him the chance to come and work for the summer at their site in the UK (see box).
Scouted and recognised by Google
Not long afterwards, he was announced as one of the winners of the PhD Fellowship awarded by Google, in the Privacy and Security category. This grant will enable him to travel to any international conferences he may wish to attend and to visit the company’s headquarters in Mountain View, California.“This sort of distinction really stands out on a young researcher’s CV. Google recognised the quality of my research and have opened their doors to me, without asking for anything in return. That’s something I won't forget, even if I’m looking more towards a career in academic research.”
We can understand why. Research into cryptographic protocols is regularly driven by updates to new defects or new types of attack. At the same time, connected objects are becoming increasingly commonplace, playing a major role in our daily lives.“The aim of my research is to enhance the trust of users; to ensure that, thanks to our verification tools, cryptographic protocols are able to offer the best possible guarantees in terms of security.”
*DEciding Equivalence Properties for SECurity protocols
A summer at Microsoft
In the summer of 2019, Itsaka Rakotonirina spent three months at Microsoft Research in Cambridge (United Kingdom). He was in charge of a new communication protocol and supplying it with security proofs. Guiding production in this way, in accordance with security criteria, helps bring about far more robust systems, even if it does require significantly more development work from the outset.