安全协议模型检验中基于消息检测的状态空间缩减
State Space Reduction with Message Inspection in Security Protocol Model Checking
摘要：
模型检验是一种广泛应用的自动形式化分析方法，它成功地发现了安全协议中的缺陷。然而，状态空间爆炸的可能性仍然阻碍了复杂协议和协议配置的分析。消息检测是一种技术，它可以在不排除可能的攻击的情况下，根据入侵者模型来划分状态空间的分支。在初步模拟中，入侵者模型使用特定元数据标记窃听的消息，从而验证可能的攻击行为的可行性。然后，消息检查算法根据这些元数据决定根据已知的安全原则哪些攻击肯定会失败。因此，先验已知的是，即如果入侵者不知道正确的密钥，则加密方案攻击不能成功。仿真以可以安全移除的攻击动作的报告终止，从而产生具有减小的状态空间的模型。
英文摘要：
Model checking is a widespread automatic formal analysis that has been successful in discovering flaws in security protocols. However existing possibilities for state space explosion still hinder analyses of complex protocols and protocol configurations. Message Inspection, is a technique that delimits the branching of the state space due to the intruder model without excluding possible attacks. In a preliminary simulation, the intruder model tags the eavesdropped messages with specific metadata that enable validation of feasibility of possible attack actions. The Message Inspection algorithm then decides based on these metadata, which attacks will certainly fail according to known security principles. Thus, it is a priori known that i.e. an encryption scheme attack cannot succeed if the intruder does not posses the right key in his knowledge. The simulation terminates with a report of the attack actions that can be safely removed, resulting in a model with a reduced state space.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
