Provided by: CNRS
Date Added: Dec 2013
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.