一种基于状态扩展的安全协议验证机制

State-extended based verification mechanism for security protocols

基于模型检测验证协议的方法存在状态空间爆炸问题,其中基于目标绑定搜索状态空间的方法有效控制了状态空间,但不能完全给出协议的运行情况。针对这一问题,提出了一种基于状态扩展的安全协议自动化验证机制,首先对协议状态进行初始搜索,给出协议运行需要的事件,得到协议基本状态,然后进行扩展搜索,考虑基本状态与其他协议运行的关系,形成协议扩展状态。该机制能够有效反映出协议的运行情况,且能够同时对多种安全性质进行验证。

The tools for cryptographic protocols analysis based on state exploration had the problem of state exploration, among them, the goal binding could deduce the states effectively, but if it couldn’t give the runs of protocol wholly. To solve this problem, this article proposed a state extended-based verification mechanism, which got the basic states with necessary events through basic search, and then proceeded with extended search in order to get the connections between basic states and the other runs, which formed the extended states. This mechanism can give the runs of protocol effectively, and under which can verified security properties synchronously.