1、浅谈无可信第三方的身份认证协议摘 要：以 ISO/IEC 11770-2 密钥建立机制为例，对无可信第三方的身份认证协议进行研究，进行严格的形式化分析和安全性能分析，发现其在不可否认性方面存在一定的缺陷，并提出了改进的方案，进一步增强了协议的安全性能。 关键词：无可信第三方；身份认证；形式化分析 引言 随着移动互联网的飞速发展，各种互联网服务给人们带来了便利，其安全问题也成为一个社会关注的焦点。身份认证是确保网络应用安全的第一道关卡，已成为当前信息安全领域的研究热点之一。 根据协议中可信第三方的参与情况，可以将身份认证协议分为有可信第三方的和无可信第三方的两大类1。在有可信第三方的身份认证协议
2、中，协议的交互需要借助可信的第三方来认证用户的身份，通常需要用户在第三方处进行相关的信息注册，可信第三方与每个用户都分别有共享的秘密信息。在无可信第三方的身份认证协议中，双方进行身份认证不需要可信第三方的参与，仅通过交换消息便可进行实体认证，协议执行中用于加密消息的密钥需要保存在双方本地。如果使用对称加密体制，需要各用户之间存在共享的密钥。 文章着重研究的无服务器密钥建立协议，是一种非常典型的无可信第三方身份认证协议，协议双方不利用服务器而直接完成双向认证并成功交换密钥。ISO/IEC 11770-2 密钥建立协议2是其中的典型，一共定义了 13 种密钥建立机制，前 6 种密钥建立机制不需要可
3、信第三方的参与。文章重点对其第 6 种密钥建立机制进行深入的分析，运用 BAN 逻辑对其进行严谨的形式化分析，发现其存在的缺陷，并提出相应的改进方案。 1 ISO/IEC 11770-2 密钥建立机制 6 ISO/IEC 11770-2 密钥建立机制 6 使用对称加密体制，涉及两个主体A 和 B，均拥有长期共享的密钥 Kab，通过引入随机数来保持信息的新鲜性，具体过程如图 1 所示。 （1）BA：Nb B 向 A 发出通信请求，发送随机数 Nb。 （2）AB：Na，Nb，B，FabKab A 收到来自 B 的请求后，用与 B长期共享的密钥 Kab 加密消息Na，Nb，B，Fab发送给 B，其中
4、随机数Na、Nb 用以标识该会话信息的新鲜性，B 为身份区分标识符，密钥材料Fab 用来后继生成会话密钥 K。 （3）BA：Nb，Na，FbaKab B 将收到的消息解密，通过核对随机数 Nb 和身份标识 B 确认这是与 A 之间的会话，然后用密钥 Kab 将 Nb，Na，Fba加密后发送给 A，其中密钥材料 Fba 用来生成会话密钥 K。 通过上述 3 个步骤，会话双方 A 和 B 能够确认对方身份，并生成新的会话密钥 K=F（Fab，Fba） ，A 和 B 能借助 K 建立新的安全会话。 2 ISO/IEC 11770-2 密钥建立机制 6 的形式化分析 2.1 BAN 逻辑简介 目前广泛
5、使用的安全协议形式化分析方法是基于知识和信念的形式逻辑分析法3，其中最有影响力的是 BAN 逻辑4。BAN 逻辑是一种基于信念的模态逻辑，其目标是认证参与协议的主体的身份，分析协议能否达到预定的目标，其基本语句及其含义如表 1 所示。 BAN 逻辑的主要推理规则如下： （1）消息含义规则 R1：（P|Q P， PXK）/（P|Q|X） ，表示若 P 相信 K 为 P、Q 间的共享密钥，且 P 收到过信息XK ，那么 P 就相信 Q 曾发送过信息 X。 （2）随机数验证规则 R2：P|#（X） ，P|Q|X/（P|Q|X） ，表示若 P 相信消息 X 是新鲜的，且 P 相信 Q 曾发送过 X，那
6、么 P 就相信 Q是相信 X 的。 （3）信仰规则 R3：P|Q|（X，Y）/（P|Q|X） ，表示若 P相信 Q 相信消息（X，Y） ，则 P 相信 Q 相信 X。 （4）管辖规则 R4：（P|Q|=X，P|Q|X）/（P|X） ，如果 P相信 Q 对 X 具有管辖权，而且 P 相信 Q 相信 X，那么 P 就相信 X。 （5）新鲜性规则 R5：P|#（X）/P|#（X，Y），表示若 P 相信消息 X 是新鲜的，则 P 相信消息（X，Y）也是新鲜的。 2.2 协议的形式化分析 （1）协议的形式化描述 主体 A 和 B 之间主要通过以下三步完成认证： 1.BA：Nb；2.AB：Na，Nb，B，
7、FabKab；3.BA：Nb，Na，FbaKab （2）初始假设 A、B 相信彼此间的共享密钥 Kab：P1：A|A B；P2：B|A B； A、B 相信各自发送随机数的新鲜性：P3：A|#（Na） ；P4：B|#（Nb） ； A、B 相信彼此对密钥材料具有控制权：P5：A|B|=Fba；P6：B|A|=Fab。 （3）协议的安全目标 A、B 相信对方传来的密钥材料 Fba 和Fab：G1：A|Fba；G2：B|Fab （4）形式化分析过程 a.当 BNa，Nb，B，FabKab 时，根据初始假设 P2 和消息含义规则 R1： （B|A B，BNa，Nb，B，FabKab）/B|A|（Na，N
8、b，B，Fab）， 可得：B|A|（Na，Nb，B，Fab） （1） 即：B 相信 A 曾发送过消息Na，Nb，B，Fab。 b.根据初始假设 P4 与消息新鲜性规则 R5： B|#（Nb）/B|#（Na，Nb，B，Fab）， 可得：B|#（Na，Nb，B，Fab） （2） 即：B 相信消息Na，Nb，B，Fab的新鲜性。 c.由（1） 、 （2）和随机数验证规则 R2： B|#（Na，Nb，B，Fab） ，B|A|（Na，Nb，B，Fab）/B|A|（Na，Nb，B，Fab）， 可得：B|A|（Na，Nb，B，Fab） （3） 即：B 相信 A 相信消息Na，Nb，B，Fab的真实性。 d.
9、由（3）和信仰规则 R3： B|A|（Na，Nb，B，Fab）/（B|A|Fab） ， 可得：B|A|Fab （4） 即：B 相信 A 相信密钥材料 Fab。 e.由（4） 、初始假设 P6 和管辖规则 R4： （B|A|=Fab，B|A|Fab）/（R|P） ，可得：B|Fab，表示B 信任收到的密钥材料 Fab，安全目标 G2 得证。 同理，可推导出安全目标 G1：A|Fba。 至此，ISO/IEC 11770-2 密钥建立机制 6 的形式化分析结果表明，认证主体 A 和 B 可以实现相互之间的双向认证，可以通过密钥派生函数得到新的会话密钥 K=F（Fab，Fba） ，并能借此建立新的安全
10、会话，达到预期的目标。 3 ISO/IEC 11770-2 密钥建立机制 6 的安全性分析及改进 由上述形式化分析可以看出，ISO/IEC 11770-2 密钥建立机制 6 能够使双方主体 A 和 B 实现双向认证，双方信任收到的密钥材料并生成可信的会话密钥。但就协议的执行流程而言，在不可否认性方面存在一定的缺陷。Fab 和随机数 Na、Nb 一起组合加密发送给 B，B 通过向 A 返还Na，表明 B 收到了 A 发送给的消息，即主体 A 可以确认 B 收到密钥材料Fab。反之，B 却无法确认 A 一定收到 Fba。即如果协议第三步传输的信息丢失，主体 A 就无法收到密钥材料 Fba，也将无法
11、生成新的会话密钥，而 B 却对此一无所知。因此建议主体 A 在收到 Fba 并生成新的会话密钥K 后，回传一条信息NbK 给 B，主体 B 就可以确认 A 收到了密钥材料，从而使双方都能够确认对方能够生成新的会话密钥，同时也可以避免会话主体间的恶意否认和相互欺诈。 4 结束语 ISO/IEC 11770-2 密钥建立机制 6 作为一种简单的无可信第三方身份认证协议有着计算量小、简单易实现的优势，同时也存在适用范围有限、难以大规模使用的局限性。该协议通过长期共享的密钥来生成新的会话密钥，并通过引入随机数来保证消息的新鲜性，用于抵抗重放攻击，并使用身份标识来抵抗预重放、反射攻击。文章运用 BAN
12、逻辑对 ISO/IEC 11770-2 密钥建立机制 6 进行了严格的形式化分析，结果表明，在协议执行完整的情况下，双方主体能够实现双向认证，信任收到的密钥材料并生成可信的会话密钥。对协议的安全性分析表明，该协议无法抵御通信主体之间的恶意否认和相互欺诈，文章对此提出了改进方案，通过增加一条主体 A 返回 B 的验证性消息以抵御否认，增加协议的安全性，进一步完善了该协议。 参考文献 1卫剑钒，陈钟.安全协议分析与设计M.人民邮电出版社，2010. 2ISO/IE 1170-2.Information Technology-Security Techniques-Key Management-Part 2：Mechanisms Using Symmetric TechniquesS.1996. 3雷新锋，薛锐.密码协议分析的逻辑方法M.北京：科学出版社，2013. 4Burrrows M，Abadi M，Needham R.A logic of authenticationJ.ACM Transactions on Computer Systems，1990，8（1）：18-36.
