Title: Formal Security Proofs for Cryptographic Algorithms and Their Implementations
Speaker: David Nowak (AIST, Tokyo, Japan)
Venue:Meeting Room 334,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS
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
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.