摘 要：以ISO/IEC 11770-2密鑰建立機(jī)制為例，對無可信第三方的身份認(rèn)證協(xié)議進(jìn)行研究，進(jìn)行嚴(yán)格的形式化分析和安全性能分析，發(fā)現(xiàn)其在不可否認(rèn)性方面存在一定的缺陷，并提出了改進(jìn)的方案，進(jìn)一步增強(qiáng)了協(xié)議的安全性能。

關(guān)鍵詞：無可信第三方；身份認(rèn)證；形式化分析

引言

隨著移動互聯(lián)網(wǎng)的飛速發(fā)展，各種互聯(lián)網(wǎng)服務(wù)給人們帶來了便利，其安全問題也成為一個社會關(guān)注的焦點(diǎn)。身份認(rèn)證是確保網(wǎng)絡(luò)應(yīng)用安全的第一道關(guān)卡，已成為當(dāng)前信息安全領(lǐng)域的研究熱點(diǎn)之一。

根據(jù)協(xié)議中可信第三方的參與情況，可以將身份認(rèn)證協(xié)議分為有可信第三方的和無可信第三方的兩大類[1]。在有可信第三方的身份認(rèn)證協(xié)議中，協(xié)議的交互需要借助可信的第三方來認(rèn)證用戶的身份，通常需要用戶在第三方處進(jìn)行相關(guān)的信息注冊，可信第三方與每個用戶都分別有共享的秘密信息。在無可信第三方的身份認(rèn)證協(xié)議中，雙方進(jìn)行身份認(rèn)證不需要可信第三方的參與，僅通過交換消息便可進(jìn)行實(shí)體認(rèn)證，協(xié)議執(zhí)行中用于加密消息的密鑰需要保存在雙方本地。如果使用對稱加密體制，需要各用戶之間存在共享的密鑰。

文章著重研究的無服務(wù)器密鑰建立協(xié)議，是一種非常典型的無可信第三方身份認(rèn)證協(xié)議，協(xié)議雙方不利用服務(wù)器而直接完成雙向認(rèn)證并成功交換密鑰。ISO/IEC 11770-2密鑰建立協(xié)議[2]是其中的典型，一共定義了13種密鑰建立機(jī)制，前6種密鑰建立機(jī)制不需要可信第三方的參與。文章重點(diǎn)對其第6種密鑰建立機(jī)制進(jìn)行深入的分析，運(yùn)用BAN邏輯對其進(jìn)行嚴(yán)謹(jǐn)?shù)男问交治?，發(fā)現(xiàn)其存在的缺陷，并提出相應(yīng)的改進(jìn)方案。

1 ISO/IEC 11770-2密鑰建立機(jī)制6

ISO/IEC 11770-2密鑰建立機(jī)制6使用對稱加密體制，涉及兩個主體A和B，均擁有長期共享的密鑰Kab，通過引入隨機(jī)數(shù)來保持信息的新鮮性，具體過程如圖1所示。

（1）B→A：Nb B向A發(fā)出通信請求，發(fā)送隨機(jī)數(shù)Nb。

（2）A→B：{Na，Nb，B，F(xiàn)ab}Kab A收到來自B的請求后，用與B長期共享的密鑰Kab加密消息{Na，Nb，B，F(xiàn)ab}發(fā)送給B，其中隨機(jī)數(shù)Na、Nb用以標(biāo)識該會話信息的新鮮性，B為身份區(qū)分標(biāo)識符，密鑰材料Fab用來后繼生成會話密鑰K。

（3）B→A：{Nb，Na，F(xiàn)ba}Kab B將收到的消息解密，通過核對隨機(jī)數(shù)Nb和身份標(biāo)識B確認(rèn)這是與A之間的會話，然后用密鑰Kab將{ Nb，Na，F(xiàn)ba}加密后發(fā)送給A，其中密鑰材料Fba用來生成會話密鑰K。

通過上述3個步驟，會話雙方A和B能夠確認(rèn)對方身份，并生成新的會話密鑰K=F（Fab，F(xiàn)ba），A和B能借助K建立新的安全會話。

2 ISO/IEC 11770-2密鑰建立機(jī)制6的形式化分析

2.1 BAN邏輯簡介

目前廣泛使用的安全協(xié)議形式化分析方法是基于知識和信念的形式邏輯分析法[3]，其中最有影響力的是BAN邏輯[4]。BAN邏輯是一種基于信念的模態(tài)邏輯，其目標(biāo)是認(rèn)證參與協(xié)議的主體的身份，分析協(xié)議能否達(dá)到預(yù)定的目標(biāo)，其基本語句及其含義如表1所示。

BAN邏輯的主要推理規(guī)則如下：

（1）消息含義規(guī)則R1：（P|≡Q P， P△{X}K）/（P|≡Q|～X），表示若P相信K為P、Q間的共享密鑰，且P收到過信息{X}K ，那么P就相信Q曾發(fā)送過信息X。

（2）隨機(jī)數(shù)驗(yàn)證規(guī)則R2：{P|≡#（X），P|≡Q|～X}/（P|≡Q|≡X），表示若P相信消息X是新鮮的，且P相信Q曾發(fā)送過X，那么P就相信Q是相信X的。

（3）信仰規(guī)則R3：{P|≡Q|≡（X，Y）}/（P|≡Q|≡X），表示若P相信Q相信消息（X，Y），則P相信Q相信X。

（4）管轄規(guī)則R4：（P|≡Q|=>X，P|≡Q|≡X）/（P|≡X），如果P相信Q對X具有管轄權(quán)，而且P相信Q相信X，那么P就相信X。

（5）新鮮性規(guī)則R5：{P|≡#（X）}/{P|≡#（X，Y）}，表示若P相信消息X是新鮮的，則P相信消息（X，Y）也是新鮮的。

2.2 協(xié)議的形式化分析

（1）協(xié)議的形式化描述

主體A和B之間主要通過以下三步完成認(rèn)證：

1.B→A：Nb；2.A→B：{Na，Nb，B，F(xiàn)ab}Kab；3.B→A：{Nb，Na，F(xiàn)ba}Kab

（2）初始假設(shè)

A、B相信彼此間的共享密鑰Kab：P1：A|≡A B；P2：B|≡A B；

A、B相信各自發(fā)送隨機(jī)數(shù)的新鮮性：P3：A|≡#（Na）；P4：B|≡#（Nb）；

A、B相信彼此對密鑰材料具有控制權(quán)：P5：A|≡B|=>Fba；P6：B|≡A|=>Fab。

（3）協(xié)議的安全目標(biāo)

A、B相信對方傳來的密鑰材料Fba和Fab：G1：A|≡Fba；G2：B|≡Fab

（4）形式化分析過程

a.當(dāng)B△{Na，Nb，B，F(xiàn)ab}Kab時，根據(jù)初始假設(shè)P2和消息含義規(guī)則R1：

（B|≡A B，B△{Na，Nb，B，F(xiàn)ab}Kab）/{B|≡A|～（Na，Nb，B，F(xiàn)ab）}，

可得：B|≡A|～（Na，Nb，B，F(xiàn)ab） （1）

即：B相信A曾發(fā)送過消息{Na，Nb，B，F(xiàn)ab}。

b.根據(jù)初始假設(shè)P4與消息新鮮性規(guī)則R5：

{B|≡#（Nb）}/{B|≡#（Na，Nb，B，F(xiàn)ab）}，

可得：B|≡#（Na，Nb，B，F(xiàn)ab） （2）

即：B相信消息{Na，Nb，B，F(xiàn)ab}的新鮮性。

c.由（1）、（2）和隨機(jī)數(shù)驗(yàn)證規(guī)則R2：

{B|≡#（Na，Nb，B，F(xiàn)ab），B|≡A|～（Na，Nb，B，F(xiàn)ab）}/{B|≡A|≡（Na，Nb，B，F(xiàn)ab）}，

可得：B|≡A|≡（Na，Nb，B，F(xiàn)ab） （3）

即：B相信A相信消息{Na，Nb，B，F(xiàn)ab}的真實(shí)性。

d.由（3）和信仰規(guī)則R3：

{B|≡A|≡（Na，Nb，B，F(xiàn)ab）}/（B|≡A|≡Fab），

可得：B|≡A|≡Fab （4）

即：B相信A相信密鑰材料Fab。

e.由（4）、初始假設(shè)P6和管轄規(guī)則R4：

（B|≡A|=>Fab，B|≡A|≡Fab）/（R|≡P），可得：B|≡Fab，表示B信任收到的密鑰材料Fab，安全目標(biāo)G2得證。

同理，可推導(dǎo)出安全目標(biāo)G1：A|≡Fba。

至此，ISO/IEC 11770-2密鑰建立機(jī)制6的形式化分析結(jié)果表明，認(rèn)證主體A和B可以實(shí)現(xiàn)相互之間的雙向認(rèn)證，可以通過密鑰派生函數(shù)得到新的會話密鑰K=F（Fab，F(xiàn)ba），并能借此建立新的安全會話，達(dá)到預(yù)期的目標(biāo)。

3 ISO/IEC 11770-2密鑰建立機(jī)制6的安全性分析及改進(jìn)

由上述形式化分析可以看出，ISO/IEC 11770-2密鑰建立機(jī)制6能夠使雙方主體A和B實(shí)現(xiàn)雙向認(rèn)證，雙方信任收到的密鑰材料并生成可信的會話密鑰。但就協(xié)議的執(zhí)行流程而言，在不可否認(rèn)性方面存在一定的缺陷。Fab和隨機(jī)數(shù)Na、Nb一起組合加密發(fā)送給B，B通過向A返還Na，表明B收到了A發(fā)送給的消息，即主體A可以確認(rèn)B收到密鑰材料Fab。反之，B卻無法確認(rèn)A一定收到Fba。即如果協(xié)議第三步傳輸?shù)男畔G失，主體A就無法收到密鑰材料Fba，也將無法生成新的會話密鑰，而B卻對此一無所知。因此建議主體A在收到Fba并生成新的會話密鑰K后，回傳一條信息{Nb}K給B，主體B就可以確認(rèn)A收到了密鑰材料，從而使雙方都能夠確認(rèn)對方能夠生成新的會話密鑰，同時也可以避免會話主體間的惡意否認(rèn)和相互欺詐。

4 結(jié)束語

ISO/IEC 11770-2密鑰建立機(jī)制6作為一種簡單的無可信第三方身份認(rèn)證協(xié)議有著計(jì)算量小、簡單易實(shí)現(xiàn)的優(yōu)勢，同時也存在適用范圍有限、難以大規(guī)模使用的局限性。該協(xié)議通過長期共享的密鑰來生成新的會話密鑰，并通過引入隨機(jī)數(shù)來保證消息的新鮮性，用于抵抗重放攻擊，并使用身份標(biāo)識來抵抗預(yù)重放、反射攻擊。文章運(yùn)用BAN邏輯對ISO/IEC 11770-2密鑰建立機(jī)制6進(jìn)行了嚴(yán)格的形式化分析，結(jié)果表明，在協(xié)議執(zhí)行完整的情況下，雙方主體能夠?qū)崿F(xiàn)雙向認(rèn)證，信任收到的密鑰材料并生成可信的會話密鑰。對協(xié)議的安全性分析表明，該協(xié)議無法抵御通信主體之間的惡意否認(rèn)和相互欺詐，文章對此提出了改進(jìn)方案，通過增加一條主體A返回B的驗(yàn)證性消息以抵御否認(rèn)，增加協(xié)議的安全性，進(jìn)一步完善了該協(xié)議。

參考文獻(xiàn)

[1]衛(wèi)劍釩，陳鐘.安全協(xié)議分析與設(shè)計(jì)[M].人民郵電出版社，2010.

[2]ISO/IE 1170-2.Information Technology-Security Techniques-Key Management-Part 2：Mechanisms Using Symmetric Techniques[S].1996.

[3]雷新鋒，薛銳.密碼協(xié)議分析的邏輯方法[M].北京：科學(xué)出版社，2013.

[4]Burrrows M，Abadi M，Needham R.A logic of authentication[J].ACM Transactions on Computer Systems，1990，8（1）：18-36.