论文研究一种基于状态扩展的安全协议验证机制.pdf

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