Ludovic Robin invites you to the defense of his Phd Thesis, on Thursday the 15th of February at 10h30 in the room A008.
This defense, and the slides will be in french but feel free to come nonetheless.
Formal verification of protocols based on short authenticated strings and will take place
Modern security protocols may involve humans in order to compare or copy short strings between different devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examples of such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose a symbolic model which includes attacker capabilities for both guessing short strings, and producing collisions when short strings result from an application of weak hash functions. We propose a new decision procedure for analyzing (a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in the AKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standard.