基于抽象原则和模型检测的网络协议安全分析

Network Protocol Security Analysis Based on Abstract Principle and Model Detection

提出了一种可以缓解状态空间爆炸的抽象原则,对模型设计过程中的辅助变量、报文字段、自动状态机数量进行科学约简,在尽量不影响验证结果准确度的前提下,降低了模型的复杂度.在此基础上,提出了一种半自动化建模框架,只需用户提供少量必须的输入,不需要学习语法,就可以自动生成具有统一规范的模型,方便研究人员查阅和使用.实验结果表明,采用所提的抽象原则和半自动化建模框架创建的模型,可以验证网络协议的相关属性.

An abstract principle is proposed to mitigate the explosion of state space. The proposed scheme scientifically reduces the auxiliary variables,message fields and numbers of automatic state machines in the process of model design,and reduces the complexity and size of the model on the premise of minimizing the accuracy of verification results. A semi-automatic modeling framework is proposed thereafter,which can automatically generate models with uniform specifications with only a small amount of input provided by users and no need to learn grammar,which is convenient for researchers to consult and use.Experiments show that the model based on the proposed abstract principle and the semi-automatic modeling framework can verify the properties of the network protocol.