【文章內(nèi)容簡介】 為 AVISPA 工具集提供一個(gè)集成的 GUI界面，使其簡單易用。 AVISPA（ Automated Validation of Inter Security Protocols and Applications）是由歐洲委員會(huì)（ European Commission）資助并由歐共體的意大利、法國、瑞士和德國等國的大學(xué)或研究機(jī)構(gòu)聯(lián)合進(jìn)行的一個(gè)項(xiàng)目。項(xiàng)目啟動(dòng)于 2020 年1 月 1 日并在進(jìn)行中。項(xiàng)目的宗旨是為 Inter 上安全敏感的大型協(xié)議和應(yīng)用開發(fā)一種自動(dòng)化的和工業(yè)級的分析技術(shù) 。 [10] 下面是 AVISPA 的模塊結(jié)構(gòu)圖： 9 圖 1 .AVISPA 的工具模塊結(jié)構(gòu)圖 頂層的是 Translator HLPSL2IF（即 hlpsl 編譯器）， 它將用 HLPSL（ High Level Protocol Specification Language）語言描述的協(xié)議編譯成用 IF（ Intermediate Format）描述的協(xié)議 。 HLPSL 語言易于理解，方便用戶讀和寫 HLPSL 規(guī)范。編譯后得到的 IF描述的協(xié)議就可以輸入到底層的工具以進(jìn)行驗(yàn)證。 目前，底層的工具集包括 四個(gè) ： OFMC（ OntheFly Model Checker） 基于 CL（ Constraint Logic）邏輯的定理證明器 AtSe 基于 SAT 的模型檢測器 SATMC（實(shí)際上 SATMC 又包括三個(gè) sat Solver： Chaff、SIM 和 SATO） 樹自動(dòng)化分析器 TA4SP 事實(shí)上每個(gè)工具內(nèi)部又有相應(yīng)的編譯器將 IF 編譯成本地描述語言。 OFMC 較 Casper 的優(yōu)點(diǎn)是：不會(huì)產(chǎn)生消息空間和狀態(tài)空間的爆炸問題，協(xié)議驗(yàn)證過程所需時(shí)間非常短。這一點(diǎn)使其非常適于分析大型的工業(yè)級密碼協(xié)議 。 各工具集各有優(yōu)點(diǎn)，但在時(shí)間效率上， AtSe 要較 OFMC 要高。 另外 經(jīng)試驗(yàn)， SPAN 的 windows 版本中的底層工具子集 SATMC 是使用不了的，因?yàn)槠湟{(diào)用 的 bash shell 腳本，這腳本只能在 UNIX/LINUX 運(yùn)行。 但一般情況下，對協(xié)議的分析驗(yàn)證只需要用到 SPAN 中的 OFMC 和 AtSe 兩個(gè)工具子集就足夠了。 10 本文采用的是 windows 版本的 SPAN 程序。 當(dāng) 協(xié)議經(jīng)過底層工具集檢驗(yàn)后，程序?qū)?會(huì) 給出安全 或不安全兩種結(jié)果，對于不安全的情況將給出詳細(xì)的攻擊序列。這樣我們就能夠根據(jù)理論分析和攻擊實(shí)例來改進(jìn)協(xié)議。 注意 ：因?yàn)?SPAN 是 AVISPA 的圖形界面，為了提醒讀者這一事實(shí)： AVISPA 才是真正的自動(dòng)化分析工具，所以下文中提及 SPAN 程序統(tǒng)一使用 AVISPA 來代替， 11 第四章 使用自動(dòng)化驗(yàn)證工具分析經(jīng)典安全協(xié)議 這里我們選取了兩個(gè)經(jīng)典的協(xié)議，采用自動(dòng)化驗(yàn)證工具 AVISPA 來進(jìn)行分析，看是否有攻擊的存在，如果有是，則根據(jù)攻擊實(shí)例序列來修改協(xié)議，直至通過形式化驗(yàn)證后結(jié)果 為 Safe。同時(shí)把得出的結(jié)果與安全協(xié)議學(xué)者已得出的結(jié)果進(jìn)行比較，從而發(fā)現(xiàn) AVISPA 工具集 目前存在的一些局限性。 NSPK 協(xié)議 協(xié)議描述 NSPK 協(xié)議 [11]描述如下： ? 協(xié)議初始假設(shè)： A , B ：協(xié)議主體，相互間平等 Na， Nb ：新鮮隨機(jī)數(shù) Ka， Kb ：分別是 A, B 的公開密鑰 A 的初始知識： A ,B ,Ka, Kb B 的初始知識： A, B, Ka, Kb ? 協(xié)議步驟如下： 1) A B: { }_Kb 2) B A: { }_Ka 3) A B: { Nb }_Kb 即 ： Step1。 用戶 Alice 生成新鮮隨機(jī)數(shù) Na,并把 Na 和代表他的用戶標(biāo)識符 A 級連后，用 Bob 的公開密鑰加密后 ,發(fā)送給用戶 Bob。 Step2。 用戶 Bob 接收到 消息 { }_Kb 并解密后，把得到的 Na 和他自己新產(chǎn)生的新鮮隨機(jī)數(shù) Nb 級連， 根據(jù)解密得到的用戶標(biāo)識符 A 來選擇 用 Alice的公開密鑰 把級連后的消息 加密后發(fā)送給 Alice。 Step3。 用戶 Alice 接收到 消 息 { }_Ka 并解密后 ， 首先把解密得到的 Na 與之前他自己產(chǎn)生并保存的 Na 進(jìn)行比較，如果一致的話，則證明通信對方 12 能解讀用 bob 公開密鑰加密的信息，從而 認(rèn)為 通信對方確實(shí)是用戶 Bob，并 把 解密 得到的 Nb 用 Bob 的公開密鑰加密后發(fā)送回 Bob；如果不一致的話， 則認(rèn)為通信對方不是用戶 Bob， 中止通信。 Step4。 用戶 Bob 收到消息 { Nb }_Kb 后 ， 把解密后得到的 Nb 與 之前他自己產(chǎn)生且保存的 Nb 進(jìn)行 對比，如果一致的話，就認(rèn)為通信的對方就是用戶 Alice，從而完成 對 Alice 認(rèn)證 ，可以跟 Alice 進(jìn)行安全通信 ；不一致的話，則 認(rèn)為 認(rèn)證失敗，中斷通信。 ? 協(xié)議目標(biāo)： 1) A 和 B 相互認(rèn)證，即 A 想確認(rèn)協(xié)議運(yùn)行中的另一方確實(shí)就是其所聲稱的 B； B想 確認(rèn)協(xié)議運(yùn)行中的另一方確實(shí)就是其所聲稱的 A。 2) Na 和 Nb 的機(jī)密性，以后可以使用二者來產(chǎn)生共享的會(huì)話密鑰。 如上，協(xié)議假定雙方都知道對方的公開密鑰。 A 首先生成新鮮臨時(shí)值 Na 與其標(biāo)識符級連，用 B 的公開密鑰加密后發(fā)送給 B。 B 接收到后，生成新鮮臨時(shí)值 Nb，與Na 級連后用 A 的公開密鑰加密后發(fā)送給 A。因此 ,B 通過能讀第 1 條消息來向發(fā)起者證明自己的身份，從而響應(yīng)了發(fā)起者的請求，最后 A 通過返回用 B 的公開密鑰加密的 Nb，讓 B 檢驗(yàn) Nb 的值以確認(rèn) A 的身份。 NSPK 協(xié)議的自動(dòng)化分析 把 節(jié)中描述的 NSPK 協(xié)議 ，用 hlpsl 語言描述出來，具體編程注意事項(xiàng)請參考文獻(xiàn) [12][13]。這里就不給出完整的編碼（見論文附件 ），只給出 入侵者的初始知識和 要達(dá)到的安全目標(biāo)的 hlpsl 描述： Intruder_knowledge = { a, b, ka, kb, ki, inv(ki)} goal secrecy_of na , nb %確保 na， nb 的機(jī)密性 authentication_on bob_alice_nb %bob 憑 nb 認(rèn)證 alice end goal 注意 ： 根據(jù)協(xié)議的詳細(xì) 描述， alice 是通過某用戶能讀用 bob 的公鑰加密的信息的事實(shí)來認(rèn)證該用戶就是 bob，這一點(diǎn)已經(jīng)隱含在通信過程中。實(shí)質(zhì)上，協(xié)議設(shè)計(jì)者這 13 一想法導(dǎo)致了該協(xié)議會(huì)遭到了中間人攻擊。在下面的分析中，我們將看到這一點(diǎn)。 用 AVISPA 中的 OFCM 驗(yàn)證結(jié)果如下： % OFMC % Version of 2020/02/13 SUMMARY UNSAFE DETAILS ATTACK_FOUND PROTOCOL C:\SPAN\testsuite\results\ GOAL secrecy_of_nb BACKEND OFMC COMMENTS STATISTICS parseTime: searchTime: visitedNodes: 8 nodes depth: 2 plies ATTACK TRACE i (a,6): start (a,6) i: {Na(1).a}_ki i (b,3): {Na(1).a}_kb (b,3) i: {Na(1).Nb(2)}_ka i (a,6): {Na(1).Nb(2)}_ka (a,6) i: {Nb(2)}_ki i (i,17): Nb(2) i (i,17): Nb(2) 14 從輸出結(jié)果中 ，我們可以看到協(xié)議是 UNSAFE 的，同時(shí)知道安全目標(biāo) goal 中的secrecy_of_nb 無法滿足 ，即無法保證 nb 的機(jī)密性。然后我們詳細(xì)分析下 AVISPA 給出 ATTACK TRACE（攻擊序列）： i (a,6): start (a,6) i: {Na(1).a}_ki 這里入侵者 i 作為一個(gè)合法用戶 ，與用戶 a 開始一次合法的通信 ， a 產(chǎn)生一個(gè)新鮮臨時(shí)值 Na(1)，并用 i 的公開密鑰 ki 加密 Na(1).a 后把加密結(jié)果發(fā)給 i i (b,3): {Na(1).a}_kb (b,3) i: {Na(1).Nb(2)}_ka 入侵者 i 用自己的私 有密 鑰 inv(ki)解密從 a 接收到消息 ，并解密結(jié)果用用戶 b 的公開密鑰 kb 加密后發(fā)送給用戶 b。 b 接收 此消息后，將產(chǎn)生新鮮臨時(shí)值 Nb(2)， 并將其與 Na(1)級連后用 a 的公開密鑰 ka 加密后，發(fā)送該消息。 入侵者 i 截獲到該消息。 i (a,6): {Na(1).Nb(2)}_ka (a,6) i: {Nb(2)}_ki 入侵者 i 把截獲到的信息轉(zhuǎn)發(fā) a， a 解密消息后 ， 把 Nb(2)用 i 的公開密鑰加密后發(fā)給 i， 從而使得 i 也可以 獲知 Nb(2)。 仔細(xì)分析以上 AVISPA 給出的攻擊序列，除了獲知入侵者 i 能通過中間人攻擊來獲得 Nb 的值外 ，我們還發(fā)現(xiàn)在此協(xié)議中用戶 a 無法確認(rèn)接收 到的 消息{Na(1).Nb(2)}_ka 是否真正由正在與其通信的對方產(chǎn)生，并發(fā)送給他的，只是簡單的認(rèn)為誰把這一消息發(fā)給他，誰便是這一消息的產(chǎn)生者，而且用戶 a 回 發(fā)的信息將采用該用戶的公鑰進(jìn)行加密。我們認(rèn)為用戶 a 的這一行為正是導(dǎo)致協(xié)議遭到中間人攻擊的原因，從而使 NSPK 協(xié)議不能滿足 secrecy_of_nb，同時(shí)也 將 使另一目標(biāo)authentication_on bob_alice_nb 失敗 。 為了驗(yàn)證一點(diǎn)，我們把安全目標(biāo)改成：（具體編碼見附件 ） goal authentication_on bob_alice_nb %bob 憑 nb 認(rèn)證 alice end goal 用 AVISPA 驗(yàn)證后的輸出結(jié)果如下： 15 % OFMC % Version of 2020/02/13 SUMMARY UNSAFE DETAILS ATTACK_FOUND PROTOCOL C:\SPAN\testsuite\results\ GOAL authentication_on_bob_alice_nb BACKEND OFMC COMMENTS STATISTICS parseTime: searchTime: visitedNodes: 15 nodes depth: 3 plies ATTACK TRACE i (a,6): start (a,6) i: {Na(1).a}_ki i (b,3): {Na(1).a}_kb (b,3) i: {Na(1).Nb(2)}_ka i (a,6): {Na(1).Nb(2)}_ka (a,6) i: {Nb(2)}_ki i (b,3): {Nb(2)}_kb 整個(gè)攻擊過程與 NSPK_1 相似 ， 這 就 證明我們的想法正確，即“用戶 a 無法確認(rèn)接收到的消息 {Na(1).Nb(2)}_ka 是否真正由正在與其通信的對方產(chǎn)生，并發(fā)送給他的，只是簡單的認(rèn)為誰把這一消息發(fā)給他，誰便是這一消息的產(chǎn)生者”這一事實(shí)是導(dǎo) 16 致了 NSPK 協(xié)議遭遇中間人攻擊。下面我們就這發(fā)現(xiàn)進(jìn)行對 NSPK 協(xié)議的修改 NSPK 協(xié)議的改進(jìn) 根據(jù) 節(jié)中的分析，我們對 NSPK 協(xié)議進(jìn)行修改，修改后的協(xié)議 描 如下： ? 協(xié)議初始假設(shè)： A , B ：協(xié)議主體，相互間平等 Na， Nb ：新鮮隨機(jī)數(shù) Ka， Kb ：分別是 A, B 的公開密鑰 A 的初始知識： A ,B ,Ka, Kb B 的初始知識： A, B, Ka, Kb ? 協(xié)議步驟如下： 1) A B: { }_Kb 2) B A: {B. }_Ka 3) A B: { Nb }_Kb 即 ： Step1。 用戶 Alice 生成新鮮隨機(jī)數(shù) Na,并把 Na 和代表他的用戶標(biāo)識符 A 級連后，用 Bob 的公開密鑰加密后 ,發(fā)送給用戶 Bob。 Step2。 用戶 Bob 接收到消息 { }_Kb 并解密后，把代表 Bob 的用戶標(biāo)識符 B，解密后得到的 Na 和他自己新產(chǎn)生的新鮮隨機(jī)數(shù) Nb 級連，根據(jù)解密得到的用戶標(biāo)識符 A 來選擇用 Alice 的公開密鑰把級連后的消息加密后發(fā)送給Alice。 Step3。 用戶 Alice 接收到消息 { }_Ka 并解密后 ，首先把解密得到的 Na與之前他自己產(chǎn)生并保存的 Na 進(jìn)行比較，如果一致的話，則證明通信對方能解讀用 Bob 公開密鑰加密的信息， 并且若解密后的用戶標(biāo)識符是 Bob的標(biāo)識 B，則可 認(rèn)為通信對方確實(shí)是用戶 Bob，并把解密得到的 Nb 用 Bob的公開密鑰加密后發(fā)送回 Bob；如果不一致的話，則認(rèn)