[TYPES/announce] Postdoc position: Symbolic tools for the formal verification of cryptographic protocols

[Steve Kremer]

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 [1]

as part of the ERC Grant

SPOOC: Automated Security Proofs of Cryptographic Protocols [2]

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 [3] is a state-of-the art protocol verification tool
which has recently been extended to verify equivalence properties in
addition to trace properties. SAPIC [4] 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.

Contacts:
Jannik Dreier (jannik.dreier at loria.fr)
Steve Kremer (steve.kremer at loria.fr)

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.

Applications, including
- 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, 2019, but applications
received later may still be considered.

Informal enquiries concerning the position are welcome.

[1] https://team.inria.fr/pesto/
[2] http://homepages.loria.fr/skremer/spooc/
[3] http://tamarin-prover.github.io/
[4] http://sapic.gforge.inria.fr/