一种基于攻击序列求解的安全协议验证新算法

基于完美加密机制前提及icy攻击者模型，指出注入攻击是协议攻击者实现攻击目标的必要手段。分析了注入攻击及其形成的攻击序列的性质，并基于此提出了搜索攻击序列的算法，基于该算法实现了对安全协议的验证。提出和证明了该方法对于规则安全协议的搜索是可终止的，并通过实验实现了ns公钥协议的验证。实验结果表明，与ofmc等同类安全协议验证工具相比，该算法不仅能实现安全协议验证自动化，而且由于规则安全协议验证的可终止性，使得本算法更具实用性。