Formal Security Proofs for Cryptographic Algorithms and Their Implementations

Title: Formal Security Proofs for Cryptographic Algorithms and Their Implementations
Speaker: David Nowak (AIST, Tokyo, Japan)
Time: 3：00pm,Thursday，September 10
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 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.