关于认证测试模型教学的一些注记
2020-09-25余磊
余 磊
（淮北师范大学 计算机科学与技术学院，安徽 淮北 235000）
0 引言
安全协议是建立在密码体制上的一种消息交互协议，它运用密码算法和协议逻辑来实现身份认证、密钥分配、数据共享等安全目标，是网络空间中各种安全服务与应用的主要载体. 网络应用对安全协议功能需求的增加，使得安全协议的知识体系一直在不断地扩展与壮大. 网络空间安全一级学科的增设［1］，以及信息安全专业课程体系的持续优化和发展，为系统全面地覆盖安全协议的知识体系，“网络安全协议”已成为高校信息安全本科专业的主干课程［2］.
受安全属性需求的多样性、协议运行的高并发性、消息组织结构的复杂性、网络环境的开放性等因素影响，设计一个既没缺陷也无冗余的安全协议是一件非常复杂和困难的事情［3］，安全协议在投入使用之前必须运用已有的方法和经验对其进行正确性分析. 形式化方法已被证实是当前最为科学、严谨、有效的安全协议正确性分析方法［4］. 在网络安全上升为国家战略的时代［5］，安全协议发挥着愈来愈重要的信息安全保障作用，掌握并熟练运用一种安全协议形式分析方法，已成为信息安全本科专业人才培养规格的基本要求［6］.
在众多的安全协议形式化分析方法中由于认证测试模型在协议分析上具有方法简洁、逻辑严谨、科学有效和形式化程度较高的优点，被广泛用于安全协议的分析和设计中［7-8］. 近年来，经过众多研究人员不断地扩展、优化和完善，认证测试模型在安全协议分析上已具有较为成熟的理论和方法体系，成为安全协议形式化分析方法的典型代表. 在“网络安全协议”课程的知识体系和实践能力体系设置上，都对认证测试模型的相关知识点进行覆盖，认证测试模型理论已是“网络安全协议”的教学重点［9］. 由于认证测试模型理论涉及到代数学、图论、密码学、逻辑学和计算机语言学等多门学科内容，具有知识构成复杂、概念深奥抽象的特点，对学生的知识迁移运用能力要求较高；加上现有的认证测试理论缺乏对测试组件的密码学性质和结构性质的深入剖析，导致学生在认证测试模型的概念理解和方法应用上很难把握到位，从而成为形式化分析方法的教学难点.
关于认证测试模型研究的现有文献显示，偏重理论扩展和方法应用的科研文献颇丰［10-11］，鲜见从教学角度对认证测试理论模型相关概念和性质深入解读和探讨. 为提升认证测试模型理论的教学效果，本文结合实际教学经验，以经典的安全协议为实例，从消息组件、测试组件、认证测试模型结构3个方面给出一些教学注记，以帮助学生更好理解认证测试模型理论，消除在概念理解及方法应用上的一些误区.文中涉及串空间模型理论的相关概念请参阅文献［12］，本文不再给出.
1 消息组件
消息组件是构成协议消息的基本信息单元，是协议分析和缺陷定位的主要对象. 在消息组件概念的理解上，容易混淆消息组件与消息子项、新组件与消息起源，造成概念理解错误和使用不准确.
定义1设t为消息项，若t不能分解成级联类型形式，则称t为简单项.
定义2设n为结点且sign（n）=+，t为term（n）的消息组件.（1）若对于任意前驱结点n′⇒+n，t都不是n'的子项，则称t是源发于n.（2）若消息项t在协议的串空间中有且仅有一个源发结点，则称t是唯一源发的.
定义3设t0，t为消息项，t0为简单项且t0⊏t. 若所有满足子项关系t0t1⊏t和t1≠t0的消息项t1只能为级联类型，则称t0为t的消息组件.
定义4设n为结点，t为term（n）的消息组件. 如果对于任意前驱结点n′⇒+n，t都不是n′的消息组件，则称t是结点n上的新组件.
图1 Denning-Sacco协议
注记1消息组件的类型只能为原子类型或加密类型.
任何攻击者都有能力对级联类型的消息进行拆分、重构等操作，破坏消息构成和结构次序以达到攻击目的，而这些操作对简单项是无效的，所以消息组件是协议正确性保障的重要基本信息单元. 在图1的m2=ABS{BkABT{AkABT}kBS}kAS中，则m2只包含A、B、S、{BkABT{AkABT}kBS}kAS4 个消息组件，AB、ABS、S{BkABT{AkABT}kBS}kAS等级联类型都不是m2的消息组件.
注记2消息的简单子项并不一定是消息组件.
在m2=ABS{BkABT{AkABT}kBS}kAS中，{AkABT}kBS并不是m2的消息组件. 如果{AkABT}kBS是m2的消息组件，则在m2中存 在 {AkABT}kBS⊏{BkABT{AkABT}kBS}kAS⊏ABS{BkABT{AkABT}kBS}kAS子项关系，根据定义2，{BkABT{AkABT}kBS}kAS并不是级联类型，所以{AkABT}kBS并不是m2的消息组件.
注记3结点n的新组件并不一定源发于结点n.
新组件的定义中没有对结点的符号进行限制，所以消息项t是结点n的新组件，但t并不一定源发于n. 在图1 中，m3的消息组件{AkABT}kBS为term(
2 测试组件
测试组件体现的是协议主体对消息组件的加工运算能力，是认证测试模型的核心，是实现协议安全属性和协议功能的基础. 原有认证测试理论缺乏对测试组件的组成要素、参数类型，以及协议主体角色的分析，在概念理解上容易给学生造成一些误区.
定义5设a为原子消息项，n为结点，t={h}k为term（n）的消息组件. 如果：（1）a是h的消息组件；（2）t不是协议串空间中任意其它常规结点消息组件的真子项，称t是a在结点n中的测试组件.
注记4测试值、加密秘钥和测试主体标识是构成测试组件的三要素，其中测试主体标识具有显性和隐性两种形式.
要借助测试组件实现对协议主体身份合法性的测试，则测试对象、唯一代表测试对象合法身份的信息、信息加工的载体三者缺一不可，这三者在测试组件中分别被形式化为测试主体标识符、加密秘钥和测试值. 根据定义5，从测试组件t={h}k的结构形式上，只能看出测试值a⊏h和加密秘钥k两个要素，在测试组件的概念中也没有体现测试主体标识这个要素. 这是因为测试主体在测试组件中具有显性和隐性两种形式. 在图2 的m1={NaA}kB中，A⊏{NaA}kB，主体A的身份标识是以显性形式存在m1中的. 在m2={NaNb}kA中，A并不是m2的子项，主体A的身份是以隐含形式存在测试组件的加密秘钥kA中的.kA为A的公钥，与主体A的身份存在一一对应关系，只有拥有的主体才能对{NaNb}kA进行运算.
图2 Needham-Schroeder协议
如何提取隐含在测试组件中的协议主体标识，结合文献［11］中主体身份标识符概念，可给出主体身份标识提取方法的法则.
推论1设t={h}k为测试组件，X，Y为协议主体，id(t)为t的主体标识符集合.（1）若X⊏h，则X∈id(t)；（2）若sXY⊏h，sXY为X和Y的共享秘密，则X,Y∈id(t)；（3）若k=kXY，kXY为X和Y的共享秘钥，则X,Y∈id(t)；（4）若k=kX或分别为X的公钥和私钥，则X∈id(t).
根据注记4和推论1，图2中的3个消息m1、m2、m3都满足测试组件的条件，可以确定m1的三要素为(Na,kB,{A,B})，m2的三要素为(Na,kA,A)或(Nb,kA,A)，m3的三要素(Nb,kB,B).
注记5并不是所有主体标识都是测试主体标识，测试主体标识只包含挑战主体标识和响应主体标识.
测试主体代表的是测试组件的信源和信宿，在协议安全目标实现过程中起到关键保障作用. 根据测试主体在测试组件中的地位和角色，认证测试模型中把验证主体称为挑战主体，把被验证主体称为响应主体，测试主体标识也就相应地分为挑战主体标识和应答主体标识. 当一个协议包含多个协议主体时，在测试组件除含有挑战主体标识和应答主体标识，还含有其它协议主体标识，这些主体标识只起到数据共享的辅助作用，并不影响测试组件的安全属性，可称这些主体为协商主体. 如在图1 的m3=AB{AkABT}kBS中，根据定义5，id({AkABT}kBS)={A,B,S}，m3中包含着A、B、S3个主体标识，其中A为挑战主体标识，S为应答主体标识，B是协商主体标识. {AkABT}kBS的三要素为(T,kAB,{A,S}).
注记6测试组件的加密秘钥必定隐含响应主体标识.
在测试组件{h}k中，假设a⊏h为测试值，挑战主体只能基于测试值a，通过响应主体在k或k-1上运算的唯一性来判断响应主体的合法性，即响应主体与k或k-1存在一一对应关系，所以响应主体的身份标识必然隐含在k中. 在图2中的m1，由于主体B的公钥kB是公开的，与A不存在一一对应关系，B无法通过{NaA}kB上的加密运算实现对A的合法性测试. 由于只属于主体B，所以A可以通过对{NaA}kB的解密运算验证B的合法性，所以{NaA}kB的响应主体为B，这与B隐含在秘钥kB中是一致的.
由注记6可得出性质1.
性质1设t={h}k为测试组件，如果X是隐含在k中唯一主体标识符，则X一定是响应主体标识.
根据性质1，可以判断图2中的消息组件m2和m3的响应主体分别是A和B.
3 认证测试结构
根据测试方式的不同，认证测试模型分为出测试、入测试和主动测试3种类型，相应的3个认证测试理论主要用于安全协议的认证性分析，认证性分析是通过参数一致性判断来实现. 当运用认证测试定理对协议进行参数一致性分析时，证明过程较为复杂，且不直观，学生难以掌握和运用. 协议的参数一致性、认证性和保密性之间关系复杂，概念把握不准容易造成协议分析结果错误.
定义6设结点n1和n2满足n1⇒+n2，消息项t1、t2分别为n1和n2的消息组件，且t2为n2的新组件，消息项a满足a⊏t1∧a ⊏t2.（1）若sign(n1)）=+，sign(n2)=-，则称n1⇒+n2为a的被转换边；（2）若sign(n1)=-，sign(n2)=+，则称n1⇒+n2为a的转换边.
定义7设边n1⇒+n2为a的被转换边，t={h}k是a在结点n1中的测试组件，KP为攻击者秘钥集合. 如果a唯一源发于结点n1，且k-1∉KP，则称n1⇒+n2是a在t上的出测试.
定义8设边n1⇒+n2为a的被转换边，t={h}k是a在结点n2中的测试组件，KP为攻击者秘钥集合. 如果a唯一源发于结点n1，且k∉KP，则称n1⇒+n2是a在t上的入测试.
定义9设消息t={h}k是消息项a在结点中的测试组件，sign（n）=-，KP为攻击者秘钥集合. 如果a在串空间中是唯一源发的，且k∉KP，则称结点n是a在t上的主动测试.
注记7认证测试模型基于的是挑战与应答结构，主动测试是入测试的一种特殊情况.
认证测试模型的核心思想是协议的一方借助测试值向另一方发起消息运算挑战，然后根据对测试值的运算反馈，来判断另一方的存在性和身份的合法性，所以整个认证过程就是测试值的挑战与应答过程. 在认证测试模型中称发起测试值运算挑战的一方为挑战主体，接受测试值运算挑战的一方为响应主体. 在认证测试3种模型的定义和定理中，只有出测试和入测试中存在挑战与应答结构，但主动测试比较特殊，结构中只存在应答不存在挑战. 这主要是因为主动测试的测试值不同于出测试和入测试，出测试和入测试的测试值是由挑战主体生成的，而主动测试的测试值是测试主体双方共享的，一般为时间戳，所以在主动测试结构中就缺省测试值的挑战步骤，从形式上好像是响应主体主动发起的认证测试，顾名思义，把这种结构叫做主动测试模型. 如果把测试值共享看作协议主体发起的隐性挑战，则主动测试其实就是入测试的一种特殊情况.
注记8测试组件参数是判断协议一致性的主要依据，测试组件的参数可以分为测试主体标识参数、新鲜值参数、秘钥参数和协商数据参数4种类型. 非加密秘钥和协商主体标识为协商数据参数.
运用认证测试模型的3个定理对安全协议进行分析时，最终归结到挑战主体与响应主体在串参数的一致性判断上，测试组件的参数正是串参数一致判断的核心依据. 根据测试组件中参数的功能和作用，可以把测试组件的参数分为测试主体标识参数、新鲜值参数、秘钥参数和协商数据参数4种类型. 测试主体标识参数决定参与测试的协议主体是谁；新鲜值参数主要为测试值，其主要作用是标识协议运行的轮次和确保测试组件的新鲜性，防止重放攻击和协同攻击；秘钥参数确保响应主体串的唯一性和数据的保密性；协商数据参数辅助协议实现特定的功能和安全目标. 非加密秘钥和协商主体标识只起到数据共享和信息辅助作用，不是测试组件的核心要素，属于协商数据参数范畴. 在图3 中边
图3 Amended Otway-Rees协议
由注记4、注记6和注记8可得性质2.
性质2挑战主体通过测试组件能够确认与响应主体在秘钥参数、新鲜值参数和响应主体标识参数上达成一致.
由注记4可知，秘钥参数、新鲜值和测试主体标识参数为测试组件的三要素. 由注记6可知，响应主体标识一定隐含在测试组件中. 所以挑战主体一定与响应主体在秘钥参数、新鲜值和响应主体参数具有一致性.
根据性质2，在图3 的m4中，主体A通过{NaNbkab}kAS能确认与S在串参数{A,S,Na,kAS}上具有一致性.
注记9主动测试的测试值并不一定是时间戳，也可以是能够确认当轮协议运行具有新鲜性和唯一性的随机值.
主动测试一般用于分析测试值为时间戳的认证测试结构. 在协议运行系统的时钟同步机制上，时间戳可以用来保证消息的新鲜性，防止消息重放攻击. 由于时间戳的共享省略测试值的传递过程，所以在协议设计中常常基于时间戳来实现协议主体身份的主动认证，如图1中的m2和m3. 但主动测试的测试值并不全部基于时间戳的，如果能够使协议主体确认其它数据在当轮协议中的新鲜性和在串空间中的唯一性，也可作为测试值用于构建主动测试. 在图3的m4中，可信主体S通过把Nb与Na在{NaNbkab}kAS中的绑定，使得主体A可以通过Na的新鲜性来确认Nb的新鲜性，从而使得结点
图4 CCITT X.509协议
图5 NSPK协议的内部攻击
注记10测试组件的三要素只能确保协议满足弱一致性，当且仅当在挑战主体标识和协商数据上满足一致性时，才能确保协议满足强一致性，弱一致性不能保证协议的认证性.
设A，B为某一认证协议的两个通信主体，若A要实现对B身份的认证，根据认证逻辑［15］，当A收到B发送的认证消息m时，A不仅知道m是B发送的，还要知道是针对自己发送的. 放在认证测试模型中，只有挑战主体标识和响应主体标识同时包含测试组件中，才能确保挑战主体对响应主体的正确认证. 即只有挑战主体与响应主体在挑战主体标识、响应主体标识、新鲜值和密钥参数上达成一致性，协议才满足认证性. 如果挑战主体还能进一步与响应主体在协商数据上满足一致性，则协议满足强一致性.弱一致性容易遭受来自协议内部的协同攻击，无法保证协议的认证性. 图5为NSPK协议的内部攻击丛图，I为内部攻击者，冒充A向B发起身份认证，A可以通过测试组件{NaA}kI能实现对I的正确认证，但是B无法通过测试组件{NaNb}kA实现对A的正确认证. 导致NSPK存在攻击的主要原因是，{NaNb}kA
中缺少挑战主体B的标识符，B与A不能在挑战主体标识符B上达成一致.
由性质2可知，挑战主体通过测试组件只能确保与应答主体在响应主体标识，新鲜值和密钥参数上具有一致性，而不能确保在挑战主体标识和协商数据上的一致性，故测试组件的三要素只能确保协议的弱一致性.
4 结论
认证测试模型的上述教学注记既涉及到概念的剖析和性质挖掘，又涉及到方法的优化和萃取. 对测试组件的组成要素、参数类型和主体角色的深入剖析，进一步加深学生对认证测试模型结构性质和密码学性质的理解. 对消息子项与消息组件、新组件与消息起源、显性主体标识和隐形主体标识、挑战主体与应答主体、时间戳与随机值、一致性与认证性、认证性和保密性等概念关系的辨析，可以消除学生在概念理解和方法应用上存在的误区，提高认证测试模型概念使用的准确性和方法应用的严谨性. 对串参数一致性判断方法、协议认证性分析方法、认证测试结构判断和设计方法的优化，以及对主体标识符提取方法、协议保密性分析方法的扩展，让认证测试方法变得更加简洁、具体和直观，让学生更加易于理解、掌握和运用，能够有效提升认证测试模型的教学效果.
