Mihhail Aizatulin (Russian: Михаил Айзатулин)
PhD Student

Computing Department
2nd Floor, Jenny Lee Building,
The Open University
Walton Hall
Milton Keynes, MK7 6AA
United Kingdom

Email: avatarAThotDOTee


I'm a PhD student at the The Open University supervised by Andrew Gordon, Jan Jürjens and Bashar Nuseibeh. I am working on a static analysis tool for cryptographic security properties of C programs. The aim is to automatically check for violations of secrecy and authentication in protocol implementations like OpenSSL, GnuTLS or Kerberos. François Dupressoir works on the same problem using a different approach.

The current method uses symbolic execution of the C code to extract a model which can then be analysed either in the symbolic setting [AGJ2011] using ProVerif or in the computational setting [AGJ2012] using CryptoVerif. The implementation is available for download.





Last Updated: 15.02.2012