论文部分内容阅读
针对当前基于树自动模型检测工具不能构造攻击路径的问题，提出一种新的安全协议自动化检测系统 TAVS。该系统能够存储临界对和推理轨迹信息，并采用回溯算法自动地构造相应的攻击路径。通过对LPD-IMSR协议进行检测，TAVS系统发现两个新的中间人攻击，并输出了相应的攻击路径。针对这两个攻击，提出改进方案并作了进一步测试，测试结果表明了改进协议的安全性。“,”Since most of the current model checking tools based on tree automata can not construct intruder paths, a new automatic verification system for security protocols named TAVS is proposed. The new system can store the information of critical pairs and induction traces, and construct the corresponding intruder paths automatically using backtracking algorithm based on these information. By verifying the LPD-IMSR protocol, TAVS finds two new man-in-the-middle attacks, and outputs the corresponding paths simultaneously. In order to prevent these two attacks, an improved scheme is presented and reverified. The test results show that the improved scheme is secure.