关键词: 密码分析，计时攻击，形式化表达

Abstract: The sidcchanncl attacks take advantage of physical characteristics leaking from side channel of implementa- lion in cipher device to recover the key or other secret parameters involved in the computation running in the cipher de- vice, which blazes a new path distinct from conventional cryptanalysis methods. Equivalence relation and ectuivalence class were adopted in formal qualitative analysis against timing attacks, one type of sidcchannel attacks. hhe method of measurement in information entropy was adopted in quantitative evaluation on timing-attack ability. Formal analysis was conducted on timing attacks against RSA binary modular exponentiation algorithm, indicating that formal analysis on timing attacks could make the attack procedure intuitive and accurate, thus providing valuable reference for formal de- scription of other side channel attack approaches.

Key words: Cryptanalysis,Liming attacks,Formal approaches