分析安全协议猜测攻击的模态逻辑方法

Modal Logic Approach for Analyzing Security Protocol Guessing Attacks

以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和Vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击相关的定理以反映在线猜测攻击的特点;通过相关引理和定理的证明,简化了猜测攻击的分析过程,使该文方法比现有方法更加简洁高效.扩展后的逻辑能够用于分析安全协议的猜测攻击,包括在线猜测攻击.

In the field of security protocol formal verification, it is a new challenge to analyze security protocol guessing attacks. CKT5 logic, used as the base, is significantly extended in several aspects. Both public key cryptography and Vernam encryption are added to symmetric key cryptography of the original logic, which makes it more powerful in expressing security protocols. Perfect encryption hypothesis is not obeyed any more, and a series of definitions and rules are given to allow principals to guess and verify passwords. Theorems and lemmas given in this paper can describe features of on-line guessing attacks, and simplify the analysis procedure of guessing attacks. The extended logic can be used to analyze guessing attacks on security protocols including on-line guessing attacks.