Formally Proved Security of Assembly Code Against Power Analysis
In the authors keynote speech at CHES 2004, kocher advocated that side-channel attacks were an illustration that formal cryptography was not as secure as it was believed because some assumptions (e.g., no auxiliary information is available during the computation) were not modeled. This failure is due to the fact that formal methods work with models rather than implementations. In this paper they present formal methods and tools for designing protected code and proving its security against power analysis.
Provided by: CNRS Topic: Security Date Added: Dec 2013 Format: PDF