under the supervision of Gilles Barthe. I am currently working at the newly-founded MPI in Bochum, and my current projects try to connect the symbolic techniques I developed during my thesis to other areas of security than cryptographic protocols.
under the supervision of Steve Kremer and Vincent Cheval. I developed and implemented symbolic techniques for formalising and analysing automatedly security protocols. I typically contributed to the theory and development of the DeepSec prover for analysing privacy-type properties.
under the supervision of Antoine Delignat-Lavaud and Cédric Fournet. I worked on the formal specification, implementation and proof of the IETF version of the QUIC protocol (still in standardisation at the time of the internship). I contributed to this long-time effort by writing proofs for the packet parsing/encryption of QUIC, using the F* proof assistant.
under the supervision of Boris Köpf. I studied and formalised the information leakage of cryptographic secrets to attackers measuring the execution time of sensitive programs.