Postdoc: Symbolic tools for the formal verification of cryptographic protocols
A 12-month position for post-doctoral research on
Symbolic tools for the formal verification of cryptographic protocols
is available at the Inria Nancy / LORIA research center within the Inria project team
PESTO: Proof techniques for security protocols 
as part of the ERC Grant
SPOOC: Automated Security Proofs of Cryptographic Protocols 
Security protocols are distributed programs that aim at ensuring security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the Internet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness.
One generally distinguishes two families of security properties: trace properties and observational equivalence properties. Trace properties verify a predicate on a given trace and are typically used to express authentication properties. Observational equivalence expresses that an adversary cannot distinguish two situations and is used to model anonymity and strong confidentiality properties.
The Tamarin prover  is a state-of-the art protocol verification tool which has recently been extended to verify equivalence properties in addition to trace properties. SAPIC  allows protocols to be specified in a high-level protocol specification language, an extension of the applied pi-calculus, and uses the Tamarin prover as a backend by compiling the language into multi-set rewrite rules, the input format of Tamarin. Tamarin and SAPIC have been successfully used to verify standards such as TLS 1.3 and 5G AKA as well as industrial protocols such as OPC UA. The objective of this postdoc is to contribute to the development of the SAPIC/Tamarin toolchain, work on extensions and use the tool(s) to analyse particular classes of protocols.
Successful candidates must have defended a PhD in computer science, or expect to defend their PhD before taking up the position. Expected qualifications are:
– solid knowledge of logic, proofs and/or formal verification techniques,
– solid programming experience, ideally with functional programming in OCAML or Haskell.
Security knowledge is not required, but a plus.
Jannik Dreier (firstname.lastname@example.org)
Steve Kremer (email@example.com)
Duration: 12 months (possibility to extend for another 12 months)
Starting date: September 1, 2019 (earlier date negociable)
The position is located at the Inria Nancy / LORIA research center in Nancy, France, with over 430 researchers, engineers and technicians. Nancy is a young (more than 45,000 students) city in eastern France with a rich cultural life and a high quality of life. It is famous for its Unesco World Heritage Site “Place Stanislas”. Paris is only 1h30 by TGV, Luxembourg, Germany and the Vosges mountains less than 1h30 by car.
– a motivation letter including your scientific and career projects,
– a CV describing your research activities (max. 2 pages),
– a short description of your best contributions (max. 1 page for max. 3 contributions including theoretical research, implementation or industry transfer),
– your two best publications,
– if you have not defended yet, the list of expected members of your PhD committee and the expected date of defense,
should be sent to the the addresses indicated above as two pdf files (one for the publications, the other for the other documents).
Additionally, at least one recommendation letter from your PhD advisor(s), and up to two additional letters of recommendation should be sent directly by their authors to the email addresses indicated above.
Applications should be received by June 30, 2018, but applications received later may still be considered.
Informal enquiries concerning the position are welcome.