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.