摘要：建立在协议主体参数新近一致性上的主体关联度由于能够正确反映协议安全属性与协议结构、消息组件和消息参数的逻辑关系,因此不仅能够为安全协议的正确性分析提供准确严谨的形式化判断依据,还能进一步降低协议分析的复杂度。为此,文章提出一种基于主体关联度的安全协议形式化分析方法。该方法首先在认证测试模型上,通过对消息组件的参数分类,给出协议主体关联度的量化定义;再根据认证测试规则和测试组件上的参数一致性判定条件,建立协议关联性、认证性、协商数据一致性与协议主体关联度的逻辑关联;接着在协议主体关联度上实现对安全协议设计目标的正确性分析。文章运用该方法对Neuman-Stubblebine协议进行分析,准确发现了协议中潜在的隐患及其根源,并证实了协议主体关联度在安全协议正确性分析中的应用可行性和有效性。