[9-10]Formal security proofs for cryptographic algorithms and their implementations

Date:2009-09-07

Title:  Formal security proofs for cryptographic algorithms and their implementations
Speaker:  David Nowak (AIST, Tokyo, Japan)
Date: 3pm, Thursday September 10
Venue: Lecture room 334, the 3rd floor, Building #5, State Key Lab of Computer Science
ABSTRACT:
With today’s dissemination of embedded systems manipulating sensitive data, it has become important to equip low-level programs with strong security guarantees. In this talk I will first present the toolbox that I have implemented on top of the proof assistant Coq for writing and checking game-based security proofs of cryptographic algorithms;  then I will show how it has been integrated with a framework in Coq for correctness proofs of assembly programs in order to guarantee the security of implementations in assembly language of cryptographic algorithms.