摘要: 本文讨论和建立了一种状态空间探寻式（SEV）协议验证问题的图论模型，并形式地定义了协议错误、协议正确程度、验证算法复杂度等概念．本文提出了一个基于启发式搜索的协议验证算法 Z^*，并就其复杂度同耗尽式验证算法 Breadfirst 进行了比较．