on March 16, 2023 at 2:00 pm
Cryptographic protocols everywhere – Are we well protected?
Security protocols are widely used today to secure transactions that take place through public channels like the Internet. Typical functionalities are the transfer of a credit card number or the authentification of a user on a system. Because pf their increasing ubiquity in many important applications (e.g. electronic commerce, smartphone, government-issued ID…), a very important research challenge consists of developing methods and verification tools to increase our trust in security protocols, and so on the applications that rely on them.
Formal symbolic methods offer a way to carefully analyse security protocols through the development of proof techniques and specific tools, e.g. ProVerif, and Tamarin. These methods build on techniques from model-checking, automated reasoning, and concurrency theory. We will explain how security protocols as well as the security properties they are supposed to achieve are formalised in those symbolic models. We willreview existing results and also point out their main limitations. Then, we will briefly present the Squirrel prover, a recent interactive tool partly developed by the Spicy team. This tool is based on the so-called computational model and offers stronger security guarantees than the one obtained in the symbolic setting.
More...Amphi Ircica – 50 avenue Halley – Haute Borne – Villeneuve d’Ascq
français
English