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