安全協(xié)議的形式化驗證與分析已成為國際研究的熱點。本文應(yīng)用BAN 邏輯研究
Needham-Schroeder 對稱密鑰認證協(xié)議，指出該協(xié)議存在的安全缺陷，利用消息新鮮性對其進行相應(yīng)改進，并在BAN 邏輯下形式化證明改進的協(xié)議可以滿足安全目標(biāo)。
關(guān)鍵詞 安全性分析；形式化；BAN 邏輯；認證協(xié)議
通信協(xié)議的安全是網(wǎng)絡(luò)信息安全的基礎(chǔ)，但僅根據(jù)以往的經(jīng)驗設(shè)計或分析驗證一個安全
協(xié)議是十分困難的，因此我們必須借助形式化方法。近20 年來涌現(xiàn)了很多形式化研究方法，其中基于知識和信仰的模態(tài)邏輯方法由于其簡單、實用、抽象度高等特點在安全協(xié)議驗證方面獲得了廣泛的應(yīng)用。邏輯方法中BAN 邏輯是一項開創(chuàng)性的工作，GNY 邏輯、AT 邏輯、VO 邏輯和SVO 邏輯等都是對BAN 邏輯的擴展[1]。Needham-Schroeder 協(xié)議由Needham 和Schroeder 在1978 年提出，是最為著名的早期的認證協(xié)議[2]，該協(xié)議可分為對稱密碼體制和非對稱密碼體制下兩個版本。在此只關(guān)注對稱密鑰體制下的Needham-Schroeder 協(xié)議（以下簡稱為NS 協(xié)議），它是一種具有可信第三方的對稱密鑰分發(fā)協(xié)議。Denning 和Sacco 在1981年指出該協(xié)議存在安全缺陷可以對其進行重放攻擊[3]，但提出的改進方案仍存在問題。我們應(yīng)用BAN 邏輯研究NS 協(xié)議的安全缺陷發(fā)現(xiàn)，該缺陷由缺乏消息新鮮性引起，容易被協(xié)議設(shè)計者忽視，其他協(xié)議如Yahalom 協(xié)議也存在類似安全缺陷。本文分析了如何改進，給出改進后的協(xié)議，并用BAN 邏輯證明了改進的協(xié)議可以滿足安全目標(biāo)。