The PESTO Team at INRIA Nancy-Grand Est aims at building formal models and techniques for computer-aided analysis and design of security protocols. We have an open Ph.D. research position and are looking for an enthusiastic Ph.D. candidate to work on the SAPIC/Tamarin security protocol verification tool chain. Possible projects include supporting more cryptographic primitives, improving the verification of privacy-type properties, or investigate novel and promising applications. The candidate should have a good knowledge of logic (deduction, trees, proofs), and should not be afraid of writing proofs. For the implementation part, a good command of Haskell, OCaml, or a similar functional language is necessary. Security knowledge is not mandatory, but a plus. Application deadline: March 1, 2017. Start date: September 1, 2017 Duration: 3 years For more information on the projects, see the full offer at https://members.loria.fr/skremer/files/spooc/phd-sapic-tamarin.pdf The paid position (monthly salary of approximately 1.580 € net) comes with health insurance and INRIA employee benefits, and is located in Nancy, France. The project is supported by the ERC Consolidator grant SPOOC: https://members.loria.fr/skremer/files/spooc/index.html Jannik Dreier and Steve Kremer