基于ＧＳＰＭ的安全協(xié)議新鮮性分析

摘要：安全協(xié)議形式化分析方法通過規(guī)范描述和數(shù)學(xué)推理來檢驗(yàn)安全協(xié)議是否滿足各種安全要求。GSPM是安全協(xié)議形式化分析的一般模型。在該模型中加入新鮮性的定義，形式化描述了新鮮性這一特殊的安全性質(zhì)，擴(kuò)展了GSPM的適用范圍，并通過Andrew Secure RPC協(xié)議給出了形式化分析新鮮性的實(shí)例研究。

關(guān)鍵詞：安全協(xié)議； 新鮮性； 一般安全協(xié)議模型

中圖分類號(hào)：TP309文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：1001-3695(2007)11-0143-03

在互聯(lián)網(wǎng)應(yīng)用日益廣泛的今天，安全協(xié)議已成為人們傳輸文件、遠(yuǎn)程會(huì)話、電子商務(wù)等網(wǎng)絡(luò)通信中不可或缺的組成部分。安全協(xié)議是建立在密碼體制基礎(chǔ)上的一種高互通協(xié)議，運(yùn)行在計(jì)算機(jī)通信網(wǎng)或分布式系統(tǒng)中，為安全需求的各方提供一系列步驟，借助于密碼算法來達(dá)到密鑰分配、身份認(rèn)證、信息保密以及安全完成電子交易等目的。然而，設(shè)計(jì)一個(gè)正確、符合安全目標(biāo)的協(xié)議十分困難。一些著名的安全協(xié)議在使用了相當(dāng)長的時(shí)間后，相繼被發(fā)現(xiàn)存在安全漏洞。傳統(tǒng)的通過直覺觀察的手段分析協(xié)議安全性的方法已不能滿足需要。因此，使用形式化的方法分析安全協(xié)議越來越引起人們的關(guān)注，已成為當(dāng)前安全協(xié)議研究的熱點(diǎn)[1]。

一般安全協(xié)議模型（GSPM）是以進(jìn)程演算為基礎(chǔ)、結(jié)合協(xié)議主體知識(shí)的邏輯推理而建立起來的一個(gè)可以精確刻畫安全協(xié)議的框架[2]。GSPM系統(tǒng)實(shí)現(xiàn)了安全協(xié)議的保密性、認(rèn)證性、公平性等絕大多數(shù)安全性質(zhì)的描述與驗(yàn)證，并能對(duì)有漏洞的協(xié)議指出可能引發(fā)的黑客攻擊。但是，GSPM未涉及時(shí)間上的語義，對(duì)于一類特殊的安全性質(zhì)——新鮮性，GSPM無法加以描述。因此，帶有新鮮性缺陷的協(xié)議在已有的GSPM系統(tǒng)中無法檢測(cè)出潛在的漏洞。在其他已有的安全協(xié)議形式化模型中，也都尚未出現(xiàn)對(duì)新鮮性的研究[3，4]。

本文對(duì)GSPM加以擴(kuò)展，給出了新鮮性的形式化定義與證明。與新鮮性相關(guān)的漏洞也將能在GSPM系統(tǒng)中檢測(cè)得到。

1一般安全協(xié)議模型

一般安全協(xié)議模型以進(jìn)程演算為基礎(chǔ)，結(jié)合協(xié)議主體知識(shí)的邏輯推理，可以精確刻畫安全協(xié)議，在統(tǒng)一的框架下形式化描述和驗(yàn)證多種安全性質(zhì)，是一種面向安全協(xié)議分析的進(jìn)程演算模型。

GSPM使用消息空間的概念，將網(wǎng)絡(luò)通信中的消息（message）分為明文、密鑰、隨機(jī)值、密文等。密鑰又分為對(duì)稱密鑰、公鑰及其對(duì)應(yīng)的私鑰。各類消息可以通過鏈接、加密和解密等計(jì)算生成新的消息。

4結(jié)束語

安全協(xié)議形式化驗(yàn)證是近年來的研究熱點(diǎn)。安全協(xié)議的新鮮性是一種特殊的安全要求，本文以一般安全協(xié)議模型（GSPM）為基礎(chǔ)，嘗試引入新鮮性的定義與描述，擴(kuò)展了GSPM的應(yīng)用范圍。以GSPM為基礎(chǔ)的自動(dòng)驗(yàn)證工具正在開發(fā)，筆者將實(shí)現(xiàn)安全協(xié)議新鮮性的自動(dòng)驗(yàn)證。

參考文獻(xiàn)：

［1］卿斯?jié)h.安全協(xié)議20年研究進(jìn)展 [J].軟件學(xué)報(bào)，2003，14(10):1740－1752.

［2］顧永跟，傅育熙.基于進(jìn)程演算和知識(shí)推理的安全協(xié)議形式化分析 [J].計(jì)算機(jī)研究與發(fā)展，2006， 43（5）:953-958.

［3］李夢(mèng)君，李舟軍，陳火旺.基于進(jìn)程代數(shù)安全協(xié)議驗(yàn)證的研究綜述[J].計(jì)算機(jī)研究與發(fā)展，2004，41(7):1093－1103.

［4］McDERMOTT J. Visual security protocol modeling[C]//Proc of the 2005 Workshop on New Security Paradigms. California: ACM Press， 2005: 97－109.

［5］DOLEV D， YAO A. On the security of public key protocols [J]. IEEE Transactions on Information Theory， 1983，29(2):198-208.

［6］SUTTON R. Secure communication：applications and management [M]. West Sussex， England: Wiley， 2002:269.

［7］CLARK J， JACOB J. A survey of authentication protocol literature ［EB/OL］. [2006-09-06].http://www.cs.york.ac.uk/jac/.

“本文中所涉及到的圖表、注解、公式等內(nèi)容請(qǐng)以PDF格式閱讀原文”