Dr Vincent Cheval
Academic subject(s):
Core subject area: Formal verification, security protocols, protocol design, automated reasoning
Research interests: My research area is the formal analysis and design of cryptographic protocols, with an emphasis on automated verification in the so-called symbolic model and the development of state-of-the-art verification tools. The theories behind my research and tools have root in automated reasoning, rewriting, (probabilistic) model-checking, first-order logic and concurrency theory. Originally, I mainly focused on privacy-type security properties such as anonymity, privacy, unlinkability, strong secrecy that can be expressed by the means of behavioral equivalences. Since 2018, through my work on ProVerif, I have tackled a broader set of security properties, including for example accountability, injective-correspondence, end-to-end verifiability, liveness. My research aims at verifying relevant security protocols, e.g. TLS, cryptocurrency blockchain based protocols, electronic voting protocols, RFID protocols, certificate management protocols, telecommunication protocols, cloud computing…