（計算機應用技術專業(yè)論文）電子商務協(xié)議形式化分析工具的研究.pdf

南京郵電學院碩士學位論文 摘要 隨著電子商務在全球的迅猛發(fā)展 電子商務的安全問題曰益受到人們的關 注 安全的電子商務協(xié)議是確保電子商務活動可靠開展的基礎 而安全協(xié)議的形 式化分析邏輯則是檢驗協(xié)議是否安全的有力工具 本文首先介紹了電子商務協(xié)議的多層安全需求模型 以及安全電子商務協(xié)議 中涉及的關鍵基礎技術 在此基礎之上 本文以最典型的b a n 邏輯和k a i l a r 邏 輯為例 對已有的形式化邏輯工具進行了深入的分析 以具體的協(xié)議分析實例說 明了它們存在的不足和缺陷 并針對這些不足和缺陷提出了一種新的形式化邏輯 工具 新工具通過對分析步驟的規(guī)范和改進 在一定程度上避免了由于不恰當?shù)?假設 不合理的理想化等原因導致的錯誤分析 通過引入了 協(xié)議的本次執(zhí)行 這一概念 能夠有效地分析出b a n 邏輯所無能為力的重放攻擊 通過對 可追 究法則 的改進和擴充 克服了k a i l a r 邏輯無法分析簽名密文的缺陷 通過增加 密鑰判斷法則 能夠形式化地證明密鑰的性能 有效地彌補了b a n 邏輯在 這方面的缺陷 新的邏輯工具可以分析協(xié)議主體問的信任關系和可追究關系 可 用于分析電子商務協(xié)議 認證協(xié)議以及密鑰分配協(xié)議等 本文最后通過一系列具 體的安全協(xié)議分析實例 驗證了新工具的性能 關鍵字 電子商務協(xié)議 認證協(xié)議 形式化分析 協(xié)議分析 b a n 邏輯 k a i l a r 邏輯 南京郵電學院碩士學位論文 a b s t r a c t a st h er a p i dd e v e l o p m e n to f e l e c t r o n i cc o m m e r c ea l lo v e rt h ew o r l d p e o p l ep a y m o r ea n dm o r ea r e n t i o nt oi t ss e c u r i t yi s s u c s s e c u r ee l e c t r o n i cc o m m e r c ep r o t o c o l s i n s u r et h er e l i a b i l i t yo ft h ee c o m m e r c eb a s i c a l l y a n df o r m a ll o g i ci st h ep o w e r f u l t o o lt ov e r i f yt h es e c u r ep r o t o c o l s t h i sp a p e r f i r s t l y i n t r o d u c e saf r a m e w o r ko ft h eh i e r a r c h ys e c u r i t yr e q u i e m e n t s a n ds o m ek e yt e c h n i q u e si nt h ee l e c t r o n i cc o m m e r c ep r o t o c o l s t h e n t h eb a n l o g i c a n dt h ek a i l a r l o g i ca r ea n a l y z e da n dt h e i rw e a k n e s sa n dl i m i t a t i o n sa r ei l l u s t r a t e d a f t e rt h a t an e wf o r m a ll o g i ct o o li sp u tf o r w a r dw h i c hm a k e si m p r o v e m e n t so f t h o s e e x i s t e n tl o g i ct o o l s n o r m a l i z i n gt h es t e p si np r o t o c o la n a l y s i s t h en e wt o o lc a na v o i d g e t t i n gw r o n gc o n c l u s i o n sc a u s e db yi l l o g i c a la s s u m p t i o n sa n di d e a l i z a t i o n u s i n gt h e c o n c e p to f t h i sr u no ft h ep r o t o c o l t h en e wt o o lc a nf i n do u tt h er e p l a ya t t a c k w h i l et h eb a n l o g i cc a n n o t e x p a n d i n gt h er u l e so na c c o u n t a b i l i t y t h en e wt o o lc a l l a n a l y z em e s s a g e sw i t he n c r y p t e dc o n t e n t sw h i l et h ek a i l a r l o g i cc a n n o t a d d i n gt h e k e yj u d g e m e n tr u l e t h en e wt o o lc a r lp r o v et h ep e r f o r m a n c eo fk e yf o r m a l l yw h i l e t h eb a n l o g i cc a n n o t t h en e wt o o lc a na n a l y z eb o t hb e l i e fa n d a c c o u n t a b i l i t y a m o n gp a r t i c i p a n t so fs e c u r ep r o t o c o l s s u c ha se l e c t r o n i cc o m m e r c ep r o t o c o l a u t h e n t i c a t i o np r o t o c o l k e y d i s t r i b u t i n gp r o t o c o l e t c a tl a s t t h ep e r f o r m a n c eo f t h en e wt 0 0 1i si l l u s t r a t e d k e yw o r d s e l e c t r o n i cc o m m e r c ep r o t o c o l a u t h e n t i c a t i o np r o t o c o l f o r m a lv e r i f i c a t i o n p r o t o c o la n a l y s i s b a n l o g i c k a i l a r l o g i c i i 南京郵電學院學位論文獨創(chuàng)性聲明 y 7 6 5 0 7 9 本人聲明所呈交的學位論文是我個人在導師指導下進行的研究 工作及取得的研究成果 盡我所知 除了文中特別加以標注和致謝的 地方外 論文中不包含其他人已經(jīng)發(fā)表或撰寫過的研究成果 也不包 含為獲得南京郵電學院或其它教育機構的學位或證書而使用過的材 料 與我一同工作的同志對本研究所做的任何貢獻均已在論文中作了 明確的說明并表示了謝意 研究生簽名 丑三丐 日期 西i j 研究生簽名 二壘日期 南京郵電學院學位論文使用授權聲明 南京郵電學院 中國科學技術信息研究所 國家圖書館有權保留 本人所送交學位論文的復印件和電子文檔 可以采用影印 縮印或其 他復制手段保存論文 本人電子文檔的內容和紙質論文的內容相一 致 除在保密期內的保密論文外 允許論文被查閱和借閱 可以公布 包括刊登 論文的全部或部分內容 論文的公布 包括刊登 授權 南京郵電學院研究生部辦理 一j 研究生簽名 j 三 生 導師簽名 日期 生 南京郵電學院碩士學位論文 前言 課題鶩景 隨著國際互聯(lián)網(wǎng)i n t e m e t 的日趨流行 電子商務已經(jīng)滲透到了社會上的各行 各業(yè)和人們的日常生活中 電子商務的發(fā)展使得企業(yè)發(fā)生劇變 無論是大企業(yè)還 是小企業(yè) 都必須努力地去爭取電子商務的成功 上網(wǎng)的企業(yè)不一定能成功 但不上網(wǎng)的企業(yè)將遲早被淘汰出局 已成為大多數(shù)人的共識 電子商務正在改變 著企業(yè)和消費者之間就企業(yè)的產(chǎn)品和服務供應而進行的交互方式 它正在為完全 嶄新的企業(yè)風險投資的孕育創(chuàng)造機會 它還促使政府部門重新思考其一貫作為傳 統(tǒng)監(jiān)督者的角色定位 電子商務已經(jīng)給各種企業(yè) 各種職業(yè) 消費者 企業(yè)家 投資者以及政府部門造成了巨大的影響 電子商務的范圍涉及全球 能夠以一種 前所未有的方式跨越國與國的邊界 盡管電子商務的發(fā)展前景十分誘人 但是人們對電子商務的安全卻普遍心存 疑慮 電子商務活動基于開放的互聯(lián)網(wǎng) 必然面臨各種安全風險 如欺詐 抵賴 信息泄漏或被篡改等等 因而在電子商務中 安全是一個至關重要的核心問題 電子商務安全涉及信息的保密性和完整性 交易身份的真實性 公平性 不可否 認性以及可審計性等等 從目前解決安全問題的方式來看 基于密碼技術的安全 協(xié)議是解決電子商務安全問題最有效的手段之一 迄今為止 國內外已經(jīng)出現(xiàn)了 大量的電子商務協(xié)議 0 1 n e t b i l l 協(xié)議 s e t 協(xié)議 s s l 協(xié)議 i k p 協(xié)議等等 然而 眾所周知 即使參加協(xié)議的主體只有2 3 個 協(xié)議交換的消息只有3 5 條 要設計一個正確 沒有安全缺陷的安全協(xié)議依然是十分困難的 經(jīng)過精心設 計的協(xié)議往往存在安全上的漏洞 因而 我們迫切需要一些強有力的工具 對安 全協(xié)議進行嚴謹?shù)姆治鲵炞C 以往對安全協(xié)議的驗證手段主要有兩類 一類是用 常艦的方法 對協(xié)議進行實際攻擊 另一類是從表面上進行直觀監(jiān)測 但是 i j i 者必須在系統(tǒng)已經(jīng)建立之后彳 能檢測出它的錯誤 后者由于檢測手段不夠嚴密 難免有疏漏之處 形式化邏輯分析工具使得我們可以在安全協(xié)議付諸實施之前 用一種嚴密可靠的方法對協(xié)議的安全性進行驗證 檢查協(xié)議是否可以達到其設計 目標 協(xié)議是否存在安全缺陷等等 安全協(xié)議的形式化分析方法是安全協(xié)議研究 南京郵電學院碩士學位論文 中最關鍵的研究問題之一 也是信息安全領域中的 個重要的研究方向 它的研 究始于8 0 年代初 目前正處于百花齊放 充滿活力的狀態(tài)之中 許多一流大學和 公司的介入 使這一領域成為研究熱點 隨著各種有效方法及思想的不斷涌現(xiàn) 這一領域在理論上正在走向成熟i 最早提出對安全協(xié)議進行形式化分析思想的是n e e d h a m 和s c h r o e d e 一2 i 他們 為進行共享和公鑰認證的認證服務器系統(tǒng)的實現(xiàn)建立了安全協(xié)議 1 9 8 1 年 d e n n i n g 署l l s a c c o 在文獻 3 中指出了n s 私鑰協(xié)議的一個錯誤 使得人們開始關注 安全協(xié)議分析 在這一領域做出突出貢獻的是d o l e v 和y a o 緊隨其后 d o l e v e v e n 年d k a r p 在8 0 年代開發(fā)了一系列的多項式時間算法 用于對一些協(xié)議的安全性 進行分析 遺憾的是 可分析的協(xié)議太有限 因此這方面工作并未得到進一步展 開 在此基礎上發(fā)展起來的大多數(shù)形式化分析工具都采用了狀態(tài)探測技術 即定 義一個狀態(tài)空間 對其探測以確定是否存在一條路徑 對應于攻擊者的一次成功 的攻擊 有些工具中用到了歸納定理推遷技術 如在n r l 協(xié)議分析器1 5 1 中 運用 此技術證明搜索的空間規(guī)模已經(jīng)可以確保安全性 在形式化分析技術出現(xiàn)的早期 階段 它已成功地發(fā)現(xiàn)了協(xié)議中的人工分析難以發(fā)現(xiàn)的缺陷 如n r l 協(xié)議分析器 發(fā)現(xiàn)y s i m m o n s 的選擇性廣播協(xié)議的缺陷 l o n g l e y r i g b y t 具發(fā)現(xiàn)t b a n k i n g 協(xié) 議的缺陷 等等 1 1 盡管如此 直到1 9 8 9 年b u r r o w s a b a d i 年n n e e d h a m 提出了b a n 邏輯 6 1 之后 才打破了形式化分析技術這一領域的神秘感 并從此逐漸引起人們廣泛的關注 b a n 邏輯采用了與狀態(tài)探測技術完全不同的方法 通過對安全協(xié)議的運行進行 形式化分析 柬研究認證雙方如何通過相互發(fā)送和接收消息的方式 從最初的信 仰逐漸發(fā)展到協(xié)議運行最終要達到的目的 認證雙方的最終信仰 b a n 邏輯 的成功極大地激發(fā)了密碼學家對安全協(xié)議形式化分析的興趣 并導致許多安全協(xié) 議形式化分析方法的產(chǎn)生 從大的方面講 在協(xié)議形式化分析方面比較成功的研究思路可以分為三種 第一種思路是基于推理知識和信念的模態(tài)邏輯 第二種思路是基于狀態(tài)搜索工具 和定理證明技術 第三種思路是基于新的協(xié)議模型發(fā)展證明正確性理論 在沿著 第一種思路的諸多方法中 最著名的就是b a n j 罡輯 6 1 及b a n 類邏輯 7 叫 以及用 于分析電子商務協(xié)議的k a i l a r 邏輯f 目前在這方面最新的研究是k i n d r e d 提出的 南京郵電學院頌士學位論文 安全協(xié)議的生成理論r v 邏輯 l 本文主要是在對b a n 邏輯和k a i l a r 邏輯討論分 析的基礎之上 針對它們存在的不足和缺陷 提出新的邏輯分析工具 本文的i 要磅究成果和論文的綴織 本文對b a n 邏輯和k a i l a r 邏輯進行了深入的分析 以具體的分析實例說明 了它們存在的不足和缺陷 并提出了一種新的形式化邏輯工具 新工具通過對分 析步驟的規(guī)范和改進 在一定程度上避免了由于不恰當?shù)募僭O 不合理的理想化 等原因導致的錯誤分析 通過引入 協(xié)議的本次執(zhí)行 這一概念 能夠有效地分 析出b a n 邏輯所無能為力的重放攻擊 通過對 可追究法則 的改進和擴充 克服了k a i l a r 邏輯無法分析簽名密文的缺陷 通過增加 密鑰判斷法則 能夠 形式化地證明密鑰的性能 有效地彌補了b a n 邏輯在這方面的缺陷 新的邏輯 工具可以分析協(xié)議主體間的信任關系和可追究關系 可用于分析電子商務協(xié)議 認證協(xié)議以及密鑰分配協(xié)議等 第一章主要討論了電子商務的定義 并簡要分析了各類電子商務協(xié)議 給出 了電子商務協(xié)議的多層安全需求模型 論述了其中的各項安全需求 對安全協(xié)議 的形式化分析技術做了概述 第二章主要介紹了安全電子商務協(xié)議中涉及的一些關鍵技術 主要有加密解 密系統(tǒng) 數(shù)字簽名 數(shù)字信封等 并在此基礎上提出安全協(xié)議形式化分析的兩個 前提 第三章詳細介紹了最為典型 最具影響力的b a n 邏輯和k a i l a r 邏輯 并深入 分析了它們存在的不足和缺陷 第四章提出了一種新的邏輯工具 新工具在b a n 邏輯和k a i l a r 邏輯的基礎 上 規(guī)范和改進了分析安全協(xié)議的具體步驟 并提出了新的邏輯構造和推理規(guī)則 巧妙地結合了b a n 邏輯平d k a i l a r 邏輯的長處 并對它們的缺陷進行了改進 最后 通過一系列具體的安全協(xié)議分析實例 驗證了新工具的性能 南京郵電學院碩士學位論文 笫一章電子商務協(xié)議及形式化分析技術 本章內容概要 本章主要討論了電子商務的定義 按協(xié)議的執(zhí)行方式對電子 商務協(xié)議進行分類 并簡要分析了各類協(xié)議 給出了電子商務協(xié)議的多層安全需 求模型 論述了其中的各項安全需求 對安全協(xié)議的形式化分析技術做了概述 1 1 電子商務及其協(xié)議 1 1 1電子商務 電子商務源于英文e l e c t r o n i cc o m m e r c e 簡寫為e c 顧名思義 其內容包含 兩個方面 是電子方式 二是商貿活動 電子商務指的是利用方便 快捷 成 本低的電子通訊方式 買賣雙方不謀面地進行各種商貿活動 聯(lián)合國國際貿易程序簡化工作組對電子商務的定義 采用電子形式開展 商務活動 它包括在供應商 客戶 政府及其參與方之間通過任何電子工具 如 e d i w e b 技術 電子郵件等 共享非結構化或結構化商務信息 并管理和完成 在商務活動 管理活動和消費活動中的各種交易 i b m 公司對電子商務的定義 瞳1 是 電子商務是在i n t e r n e t 的廣闊聯(lián)系與傳統(tǒng) 信息技術系統(tǒng)的豐富資源相互結合的背景下 應運而生的一種在互聯(lián)網(wǎng)上展開的 相互關聯(lián)的動態(tài)商務活動 電子商務有廣義和狹義之分 狹義的電子商務稱作電 子交易 主要是利用w e b 提供的通信手段在網(wǎng)上進行的交易 而廣義的電子商務 是包括電子交易在內的 利用w e b 進行的全面商業(yè)活動 如市場調查分析 財務 核算 生產(chǎn)計劃安排 客戶聯(lián)系等 所有這些活動涉及企業(yè)的內外 由上述可見 電子商務一詞并沒有精確的定義 就電子商務而言 最根本的 是 相對于傳統(tǒng)的基于紙張的商務 電子商務代表了企業(yè)與企業(yè)之間 企業(yè)與消 費者之問或者政府與其公民或企業(yè)之間的商務交易的數(shù)字化實現(xiàn) 從企業(yè)和政府 的角度來說 電子商務是激發(fā)可用性 推動性能曲線的進步 促使現(xiàn)實世界中更 多地采用那些與i c 芯片 個人電腦 因特網(wǎng)時代的通信以及先進的應用軟件包解 決方案相關的技術 這些技術的進步推動了一個全球化的 地理政治經(jīng)濟形式的 南京郵電學院碩士學位論文 嶄新社會的出現(xiàn) 而這一新社會形式的出現(xiàn)又反過來推動了技術的進步 現(xiàn)在人們所探討的電子商務主要是以e d i 電子數(shù)據(jù)交換 和i n t e m e t 來完成 的 隨著i n t e m e t 技術的日益成熟 電子商務的真正發(fā)展是建立在i n t e m e t 技術的 基礎上的 在這里 我們給出一個如圖1 1 所示的電子商務模型乃 電子商務是 客戶 c u s t o m e r 商家 m e r c h a n t 銀行 b a n k 和為各方所信任的第三方認證機構 c a c e r t i f i c a t ea u t h o r i t y 之間的信息流 資會流和物流的交互關系 各方是通過 遍及全球的 開放的但不安全的i n t e r n e t 相互聯(lián)系的 銀行 第三商認證機構 圖1 1 電子商務模型 般說宋 電子商務具有如下特性 普遍性 方便性 整體性 安全性和協(xié) 調性 我們可以從多個不同的角度對電子商務進行分類 按商業(yè)活動運作方式可 分成完全電子商務和不完全電子商務兩類 按電子商務的服務領域可分為四類 即企業(yè)對消費者 企業(yè)對企業(yè) 企業(yè)對政府機構和消費者對政府機構的電子商務 其中 企業(yè)間的電子商務是最值得關注和探討的 因為 在現(xiàn)實的物理世界中 企業(yè)問的商務貿易額是消費者直接購買的1 0 倍 按開展電子交易的信息網(wǎng)絡范圍 可分為四類 即企業(yè)內部電子商務 本地電子商務 遠程國內電子商務和全球電 子商務 1 1 2電子商務協(xié)議 所謂協(xié)議 是指兩個或兩個以上的參與方采取一系列步驟以完成某項特定的 任務 它包含3 層意思 1 1 協(xié)議至少需要兩個參與者 一個人可以通過執(zhí)行一 系列的步驟來完成一項任務 但它不構成協(xié)議 2 在參與者之間呈現(xiàn)為消息處 理和消息交換交替進行的一系列步驟 3 通過執(zhí)行協(xié)議必須能夠完成某項任務 南京郵電學院捌士學位論文 或達成某種共識 電子商務協(xié)議是為了完成電子商務活動而設計的協(xié)議 是實現(xiàn)電子商務的重 要技術基礎 它確保電子商務各參與方之間信息流的交互有規(guī)可循 從而保證各 方的利益和安全 并能控制風險 隨著電子商務的興起 人們已研究出許多電子 商務協(xié)議 已經(jīng)實現(xiàn)的主要有d i g i c a s h f i r s t v i r t u a l n e t b i l l 安全套接層協(xié)議 s s l s e c u r es o c k e tl a y e r 安全電子交易協(xié)議s e t s e c u r ee l e c t r o n i ct r a n s a c t i o n 基于公鑰體制的i b s 協(xié)議等 目前常用的主要是s s l 和s e t 1 1 3電子商務協(xié)議的分類 將安全協(xié)議進行嚴格的分類是比較困難的 一般認為 根據(jù)安全協(xié)議的執(zhí)行 方式進行分類是 種較好的基本分類方法 本文參照s c h n e i e r 的分類方法 將電子商務協(xié)議分為兩大類 逐步交換協(xié)議和可信第三方協(xié)議 1 逐步交換協(xié)議 g r a d u a le x c h a n g ep r o t o c 0 1 即參與協(xié)議的主體只有兩個 他們通過許多步驟一步一步地暴露所交換的信息 這中問又可以分自動執(zhí)行協(xié)議 和類自動執(zhí)行協(xié)議兩種 自動執(zhí)行協(xié)議 s e l f e n f o r c i n g p r o t o c 0 1 也稱自制協(xié)議 如圖1 2 所示 它不需 要任何第三方參與就能夠保證參與方之間的公平交易 保證參與方所需要的安全 性并不會產(chǎn)生任何的爭端 在執(zhí)行過程中只要協(xié)議中有一方試圖進行欺騙行為 其他各方就會在其利益受到侵害之前檢測到欺騙行為的發(fā)生 并中止協(xié)議的執(zhí) 行 但遺憾的是 在電子商務應用中暫且沒有這種可自動執(zhí)行的安全協(xié)議 而且 有關研究證明 l 對于異步執(zhí)行的公平交換協(xié)議 沒有第三方的參與無法保證 公平 也就是說不存在自動執(zhí)行的公平交換協(xié)議 參與方 參與方b 凰川洄 i 口幽i 口i 劂口l 參與片 葺 與方b 圖1 2 自動執(zhí)行協(xié)議圖1 3 類自動執(zhí)行協(xié)議 類自動執(zhí)行協(xié)議 a p p r o x i m a t e l ys e l f e n f o r c i n gp r o t o c 0 1 如圖1 3 所示 在 執(zhí)行上與自動執(zhí)行協(xié)議比較相似 也不要第三方的參與 但決不是自動執(zhí)行協(xié)議 因為這列協(xié)議只能提供概率意義上足夠的安全性 或者說 攻擊者成功的概率相 當小 這類協(xié)議的例子很多 如s e v e n 等人提出的同時簽約協(xié)議1 1 6 1 b l u m l l7 1 南京郵電學院碩士學位論文 k i l i a n 1 8 1 分別提出的硬幣拋擲協(xié)議等 從實際應用的角度來說 不能完全保證參 與方之間的公平 而且協(xié)議的應用受到相當多的限制 但在特定的場合 比如在 沒有適當?shù)目尚诺谌酱嬖诘那闆r下 這類協(xié)議也是一種選擇 2 可信第三方 t r u s t e dt h i r dp a r t y 簡稱t t p 協(xié)議 即協(xié)議主體通過可信 第三方t t p 交換消息 以保證實現(xiàn)協(xié)議的各種安全目標 根據(jù)t t p 介入的程度 與介入方式的不同 又可以分為i n l i n et t p 協(xié)議 o n l i n et t p 協(xié)議和o f f l i n et t p 協(xié)議 在i n l i n e t t p 協(xié)議中 t t p 扮演協(xié)議主體之間的中介角色 如圖1 4 所示 協(xié)議的主體之間不交換任何消息 所有消息都通過t t p 轉發(fā) 訂p 參與了協(xié)議 的每一步運行 能夠提供較好的安全服務 但是t t p 的負荷很重 而且協(xié)議的 執(zhí)行效率非常低 1 9 9 6 年提出的c o f f e y s m d h a 協(xié)議 1 9 1 便是此類協(xié)議的典型 g 警一 參與方 參與宵b參與青 參與方b 圖1 4 i n l i n e t t p 協(xié)議圖1 5 o n l i n e l v r p 協(xié)議 在o n l i n et t p 協(xié)議中 t t p 是在線的 每個關鍵的消息都通過t t p 來轉發(fā) t t p 可以檢測協(xié)議的各參與方通過它的消息 一旦出現(xiàn)異常狀況 它就可以中止 協(xié)議的執(zhí)行 此類協(xié)議又被稱為仲裁協(xié)議 a r b i t r a g e dp r o t o c 0 1 如圖1 5 所示 由于t t p 必須處理參與方的每一次關鍵性會話 可能會成為系統(tǒng)的瓶頸和攻擊 者攻擊的焦點 著名的掛號電子郵件協(xié)議 2 0 l c m p i 和c m p 2 便屬于此類協(xié)議 o f f l i n e t t p 協(xié)議又可稱為裁決協(xié) s a d j u d i c a t e dp r o t o c 0 1 如圖1 6 所示 協(xié) 議一般分成兩個部分 j 下常執(zhí)行部分和裁決部分 在薩常情況下 協(xié)議按正常部 分的步驟執(zhí)行 若在某一步出現(xiàn)了異常 則轉為執(zhí)行裁決部分 在協(xié)議中參與各 方需要交換用于裁決爭端的證據(jù) t t p 在此類協(xié)議中的介入程度最低 但從保證 參與方之間公平性的角度來看 裁決協(xié)議要略微弱一點 a s o k a n s h o u p w a i d n e r 協(xié)議 i j 是典型的o f f l i n et r p 協(xié)議 南京郵電學院碗 學位論文 參與方 參與方b 圖1 6 o f f l i n e t t p 協(xié)議 1 1 4電子商務協(xié)議的安全需求模型 安全問題是電子商務的一個至關重要的核心問題 安全的電子商務協(xié)議是目 前解決這一問題的最有效的手段 電子商務協(xié)議建立在認證協(xié)議和密鑰交換協(xié)議 的基礎之上 其安全特性分為多個層次 即包括獨立于具體協(xié)議的淺層特性 又 包括電子商務的固有特性 還包括依賴于具體協(xié)議模型的深層特性 所有這些特 性統(tǒng)稱為安全需求 2 2 圖1 7 所示便為電子商務協(xié)議的多層安全需求模型 習 亟丑臣匭 吐 圖1 7 電子商務協(xié)議的多層安全需求模型 1 基層需求 基層需求對應于認證協(xié)議和密要分配協(xié)議的安全需求 要求滿足認證性和好 的密鑰特性 認證性包括主體認證和消息認證 是整個密碼協(xié)議的基石部分 秘密性 如果一個密鑰k 被通信雙方a 與b 接收作為會話密鑰 則除非該密 鑰泄露 否則它未被入侵者i 得知 新鮮性 如果一個密鑰被通信發(fā)起者a 接收作為與接收者b 通信的會話密鑰 南京郵電學院碩士學位論文 則該密鑰必須是新鮮的 并且該密鑰仍在有效期內 專有性 如果通信主體a 或b 接收n 者的會話密鑰 則別的誠實主體以前 沒有接收到過此密鑰 抗泄露性 如果入侵者i 獲得了一些會話密鑰k l 則他不能用這些密鑰獲得 其它會話密鑰k 2 可行性 協(xié)議應該能保證可以從執(zhí)行第一條消息開始 按序執(zhí)行到最后一條 消息 協(xié)議并不必保證每次執(zhí)行總是如此 但是如果協(xié)議從不能從第一條消息進 展到最后一條消息 那么該協(xié)議是不可行的 一致性 協(xié)議的一致性包括三個方面 如果通信主體a 從b 接收了消息m 則入侵者i 或別的誠實主體以前未曾得知m 如果發(fā)起者a 從b 接收了消息m 則b 必事先向a 發(fā)送了消息m 以回答a 向b 發(fā)送的詢問 如果通信主體a 從b 接收了消 息1 1 3 則從b 至i j a 發(fā)送的此消息必須是當前的 2 中層需求 中層需求是電子商務協(xié)議固有的安全需求 它建立在消息的匹配性 連接性 認證和好的密鑰特性的基礎上 保密性 電子商務作為一種貿易手段 其信息直接代表著個人 企業(yè)或國家 的商業(yè)機密 因而要求交易消息不能被其他人截獲及讀取 沒有人能夠通過攔截 會話數(shù)據(jù)獲得賬戶信息 同時還需滿足訂單和支付信息的保密性 原子性 原子性f 2 4 1 是指整個協(xié)議 一般包括初始化階段 訂購階段 支付 階段 清算階段等 看作一個事務 保證要么全部執(zhí)行 要么全部取消 電子商 務協(xié)議的原子性分為三個等級 包括錢原子性 商品原子性和確認發(fā)送原子性 公平性 a s o k a n 關于公平性的定義 2 5 1 是 在協(xié)議執(zhí)行的任何階段 參與協(xié) 議的任何誠實主體相對于其他主體不處于劣勢 我們將公平性與主體的利益聯(lián)系 起來 把公平性分為強公平性和弱公平性 強公平性是指在協(xié)議執(zhí)行的任何階段 任何一方終止協(xié)議或誤操作 都不會使誠實主體的利益受到損失 強公平性要求 誠實主體僅依賴自身和協(xié)議而不是其他任何主體或機構來保護自身的利益 弱公 平性是指在協(xié)議執(zhí)行的某些階段 協(xié)議允許一方誠實主體的利益暫時受到某種程 度上的損失 但卻可擁有對方在協(xié)議執(zhí)行過程中生成的不可否認的證據(jù) 在以后 的爭端中 通過這些證據(jù)恢復其公平性 南京郵電學院碩士學位論文 完整性 保持貿易各方信息的完整性是電子商務應用的基礎 因為信息的完 整性將影響到貿易各方的交易和經(jīng)營策略 要預防對信息的隨意生成 修改和刪 除 同時要防止數(shù)據(jù)傳輸過程中信息的丟失和重復并保證信息傳送次序的統(tǒng)一 不可否認性 所謂的 否認 是指通信的參與方否認參與了全部或部分 的通信 為了使通信各方對他們的行為負責 安全協(xié)議要提供一種保護 使得發(fā) 送方不可否認它發(fā)送過某條消息 同時也使接受方不能否認它接受過某條消息 不可否認服務的目的是為某一特定事件的參與方提供證據(jù) 使他們對自己的行為 負責 匿名性 匿名性有三種類型 即發(fā)送者匿名性 接收者匿名性 發(fā)送者與接 收者之間的無連接性 匿名性的含義包括三個方面 信息分離 防勾結和匿名度 其中 匿名度 2 6 1 是將匿名性從絕對隱藏 可能暴露 到暴露分為若干等級 用 來衡量電子商務協(xié)議所達到的匿名程度 可追究性 是指參與協(xié)議的任何一方主體在協(xié)議執(zhí)行完畢后 能夠提供充分 的證據(jù)以解決可能出現(xiàn)的糾紛 電子商務協(xié)議的可追究性是通過發(fā)方非否認和收 方非否認這兩個基本目標 2 7 l 達到的 3 高層需求 高層需求建立在以下兩層的基礎上 包括可靠性 可用性 抗拒絕服務性 靈活性等面向具體應用的特性 可靠性即防止惡意中斷和單點故障 并能抵抗拒 絕服務 可用性指一旦合法用戶得到訪問某一資源的權限 該資源就應該能夠隨 時為他使用 而不應該將其保護起來使用戶的合法權益受到損害 在多用戶 多 個服務器的電子商務系統(tǒng)中 提高系統(tǒng)可用性還意味著用戶僅需經(jīng)一次登錄就可 以訪問任何他有權訪問的資源 靈活性要求協(xié)議可根據(jù)不同的安全需求和性能需 求選擇多種支付方式 實現(xiàn)多種支付方式的自動轉換和綜合 1 2 安全協(xié)議的形式化分析技術 安全協(xié)議的運行不是獨立的 而是處于復雜的 公開的 不安全的環(huán)境之中 因而 要設計一個正確 沒有安全缺陷的協(xié)議是十分困難的 經(jīng)過精心設計的協(xié) 議往往還是存在安全上的漏洞 這就需要對協(xié)議進行驗證和分析 安全協(xié)議的分 析方法可分為非形式化方法和形式化方法兩大類 0 南京郵電學院碩士學位論文 非形式化方法主要有實際攻擊和直觀監(jiān)測兩種 實際攻擊是利用現(xiàn)在已知的 攻擊方法對協(xié)議進行攻擊 以攻擊是否有效判斷協(xié)議是否安全 然而 現(xiàn)實中往 往還存在許多未知的攻擊方法 因此也就無法預知在這些攻擊下協(xié)議是否安全 而且這種方法必須在協(xié)議已經(jīng)實現(xiàn) 系統(tǒng)已經(jīng)建立之后才能實行 這就有可能導 致人力物力的巨大浪費 直觀監(jiān)測就是從表面上人為地對協(xié)議進行直觀的分析 顯然這種檢測手段不夠嚴密 不能深入實質 難免有疏漏之處 形式化分析方法可以在安全協(xié)議付諸實施之前 用一種嚴密可靠的邏輯分析 工具對協(xié)議的安全性進行驗證 可使協(xié)議設計者通過系統(tǒng)分析 將注意力集中于 接口 系統(tǒng)環(huán)境的假設 系統(tǒng)在不同條件下的狀態(tài) 條件不滿足時系統(tǒng)出現(xiàn)的情 況 以及系統(tǒng)不變的屬性 并通過系統(tǒng)驗證 提供協(xié)議必要的安全保證 l 簡單 地說 形式化分析是采用一種正規(guī)的 標準的方法對協(xié)議進行分析 以檢查協(xié)議 是否滿足其安全目標 應當指出的是 運用形式化分析方法分析安全協(xié)議 都只 是保證協(xié)議安全性的必要條件 而不是協(xié)議安全性的充分條件 安全協(xié)議的形式 化分析方法大致可分為三類 基于推理的結構性方法 基于攻擊的結構性方法和 基于證明的結構性方法 基于攻擊的結構性方法通常又被稱作是模型檢測法 因為用這種方法對協(xié)議 進行分析時 一般要借助于驗證有限狀態(tài)系統(tǒng)的自動化分析工具 如一般目的的 工具f d r 2 8 故障偏差精練檢測器 f a i l u r e sd i v e r g e n c e sr e f i n e m e n tc h e c k e r 和 通用狀態(tài)計數(shù)工具m u r 中以及特殊目的的n r l 分析器 5 1 年i l i n t e r r o g a t o r 2 9 等 這些 方法都是從協(xié)議的初始狀態(tài)開始 對合法主體和一個攻擊者的所有可能的執(zhí)行路 徑進行窮盡搜索 以期找到協(xié)議可能存在的錯誤 這種方法發(fā)現(xiàn)了協(xié)議的許多以 前未發(fā)現(xiàn)的新的攻擊 對協(xié)議的自動驗證和工程化設計具有指導意義 但同時它 們也存在著一些問題 最主要的問題在于 模型檢測是用于有限狀態(tài)系統(tǒng)的分析 工具 主體的數(shù)目有限 無法解決狀態(tài)空陽j 爆炸問題 如何將協(xié)議說明成有限狀 態(tài)系統(tǒng) 而又不增加或減少協(xié)議的安全性 這將是一個需要繼續(xù)研究和探索問題 基于證明的結構性方法可以分為兩類 一類是推理構造方法 另一類是證明 構造方法 推理構造方法主要有c e r v e s a t o 等學者提出的基于線性邏輯的協(xié)議驗 證方法 3 0 1 m i l l e n 等學者提出的基于邏輯規(guī)則的協(xié)議驗證方法 3 1 1 等 其優(yōu)點是 可以發(fā)現(xiàn)攻擊 并可以證明協(xié)議在多回合運行下的正確性 其缺點是需要用戶介 南京郵電學院碩士學位論文 入 無法防止狀態(tài)爆炸 證明構造方法主要有k e m m e r e r 等學者研制的i n aj o 和 i t p 3 2 1 p a u l s o n 的基于歸納的定理證明方法1 3 3 州 t h a y e r h e r z o g 和g u t t m a n 提出的串空間模型 s t r a n ds p a c e 3 扣 1 等 其優(yōu)點是可以分析無限大小的協(xié)議 不 限制主體參與協(xié)議運行的回合 其缺點是證明過程不能全部自動化 需要人工進 行 專家式 的干預 在使用范圍上受到一定的限制 基于推理的結構性方法通常又被稱為模態(tài)邏輯方法或是邏輯分析方法 是分 析安全協(xié)議最直接 最簡單的一種方法 也是迄今為止使用最為廣泛的一種方法 它是基于知識和信仰的分析方法 主要是運用邏輯系統(tǒng) 從用戶接收和發(fā)送的消 息出發(fā) 通過一系列的推理公理推證協(xié)議是否滿足其安全說明 一般其具體的分 析過程如圖1 8 所示 這些邏輯系統(tǒng)通常由一些命題和推理公理組成 命題表示 主體對消息的知識或信仰 而運用推理公理可以從己知的知識和信仰推導出新的 知識和信仰 s y v e r s o n 3 s 闡述了在安全協(xié)議的分析中 知識 信念和語義之間的 關系與相互作用 在這類方法中 最著名的就是b a n 邏輯 6 i 和b a n 類邏輯 7 9 1 b a n 1 i k el o g i c 以及用于分析電子商務協(xié)議的k a i l a r 邏輯 l 圖1 8 安全協(xié)議形式化邏輯分析過程 總的說來 安全協(xié)議的形式化分析有助于川 1 界定安全協(xié)議的邊界 即協(xié) 議系統(tǒng)與其運行環(huán)境的界面 2 更準確地描述安全協(xié)議的行為 3 更準確地定 義安全協(xié)議的特性 4 證明安全協(xié)議滿足其說明 以及證明安全協(xié)議在什么條 件下不能滿足其說明 本文主要是從基于推理的邏輯分析方法著手 對電子商務 協(xié)議的形式化分析邏輯進行研究 南京郵電學院碩士學位論文 第二章安全電子商務協(xié)議的技術理論基礎 本章內容概要 本章主要介紹了安全電子商務協(xié)議中涉及的一些關鍵技術 主要有加密解密系統(tǒng) 數(shù)字簽名 數(shù)字信封等 并在此基礎上提出安全協(xié)議形式 化分析的兩個前提 2 1 密碼技術 密碼技術是信息安全技術中的核心技術 密碼技術的起源可以追溯到幾千年 前 它在第二次世界大戰(zhàn)期間才開始流行 目前廣泛應用于網(wǎng)絡安全和電子商務 安全之中 現(xiàn)代密碼體制和傳統(tǒng)密碼體制的最大不同在于 原文的保密性不再依 賴于算法本身 而是依賴于密鑰的保密性 算法本身是公開的 也就是說 用密 碼技術保護的現(xiàn)代信息系統(tǒng)的安全性主要取決于對密鑰的保護 而不是對算法或 硬件本身的保護 即密碼算法的安全性完全寓于密鑰之中 2 1 1 密碼系統(tǒng)概述 密碼學是研究密碼系統(tǒng)或通信系統(tǒng)安全的一門學科 采用密碼技術可以隱藏 和保護需要保密的消息 使未授權者不能提取信息 被隱藏的消息稱作明文 p l a i n t t e x t 隱藏后的消息稱作密文 c i p h e r t e x t 將明文變換成密文的過程稱作 加密 e n c r y p t i o n 其逆過程 由密文恢復出原明文的過程稱作解密 d e c r y p t i o n 對明文進行加密時所采用的一組規(guī)則稱作加密算法 對密文進行解密時所采用的 一組規(guī)則稱作解密算法 加密和解密算法的操作通常都是在一組密n k e y 控制 下進行的 分別稱為加密密鑰和解密密鑰 根據(jù)密鑰的特點 將密碼體制分為對稱密碼體制和非對稱密碼體制兩種 對 稱密碼體制又稱單鑰 私鑰或傳統(tǒng)密碼體制 非對稱密碼體制又稱雙鑰或公鑰密 碼體制 本文采用對稱密碼體制和非對稱密碼體制這兩個術語 在對稱密碼體制 中 加密密鑰和解密密鑰是一樣的或彼此之問容易相互確定的 按加密方式叉可 將對稱密碼體制分為流密碼和分組密碼兩種 在流密碼中 將明文消息按字符逐 位地加密 在分組密碼中 將明文消息分組 每組含有多個字符 逐組地進行 南京郵電學院碩士學位論文 加密 在非對稱密碼體制中 加密密鑰和解密密鑰不同 從一個難以推出另一個 可將加密和解密能力分開 現(xiàn)有的大多數(shù)非對稱密碼屬于分組密碼 在消息傳輸和處理系統(tǒng)中 除了意定的接收者外 還有非授權者 他們通過 各種辦法如搭線竊聽 電磁竊聽 聲音竊聽等來竊取機密消息 稱其為截收者 他們雖然不知道系統(tǒng)所用的密鑰 但通過分析可能從截獲的密文推斷出原來的明 文 這一過程稱作密碼分析 對一個密碼系統(tǒng)采取截獲密文進行分析的這類攻擊 稱作被動攻擊 密碼系統(tǒng)還可能遭受的另一類攻擊是主動攻擊 非法入侵者主動 向系統(tǒng)竄擾 采用刪除 更改 增填 重放 偽造等手段向系統(tǒng)注入假消息 達 到損人利己的目的 所謂一個密碼是可破的 是指通過密文能夠迅速地確定明文 或密鑰 或通過明文 密文能夠迅速地確定密鑰 一個密碼通信系統(tǒng)可用圖2 1 3 9 1 表示 它由以下幾個部分組成 明文消息空 間p 密文消息空間c 密鑰空間k l 和k 2 在對稱密碼體制下k l k 2 k 此時 密鑰k 需經(jīng)安全的密鑰信道由發(fā)方傳給收方 加密變換 p c k l k l 由 加密器完成 解密變換d c p k 2 k 2 由解密器實現(xiàn) 對每一個密鑰k 1 k l k l 確定一個加密變換e 有一個匹配的密鑰k 2 k 2 k 2 確定一個解密 變換哦 使得對于一切m p 有 k e n m m 扯法八侄肴 鬻銹源k 搭線信道搭蛀信道 尹 ll 被動攻擊 密鍘信道 密碼舒折喬im t 竊聽囂 r 竺h 竺 lk l 密餅源k 圖2 1 密碼系統(tǒng)模型 對于給定的明文消息m p 和密鑰k l k l 加密變換將明文m 變換為密文c c 川 m 戶 k a 接收者利用通過安全信道傳送來的密鑰k i 對稱密碼體 制下 或用本地密鑰生成器產(chǎn)生的解密密鑰k 2 非對稱密鑰體制下 控制解密操 作d 對接收到的密文進行變換得到恢復的明文消息m t n d 川m m p t 2 足2 而密碼分析者則對截獲的密文c 進行分析變換 得到的是明文空間中的某個元素 m7 一般的 m7 m 南京郵電學院碩士學位論文 令e 2 最 p c lk l e k e d 2 鞏 c p ik 2 k 2 則稱六元組 p c k k 2 e d 為一保密系統(tǒng) 2 1 2 對稱密碼體制 所謂對稱密碼體制 又稱私鑰密碼體制 單鑰密碼體制或是傳統(tǒng)密碼體制 就是在對數(shù)據(jù)進行加密和解密時使用相同的密鑰 即使不同 也可以由一個推導 出另一個 其基本思想如圖2 2 所示 這就要求發(fā)送者和接收者在進行信息的傳 輸和處理時 必須共同持有該密鑰 i室皇笪望 圖2 2 對稱密鑰體制 常用的私鑰密碼算法有d e s s a f e rk 6 4 r c 5 i d e a 等 其中由i b m 公司提出的d e s d a t ae n c r y p t i o ns t a n d a r d 算法使用得最為普遍 被i s o 采用作 為數(shù)據(jù)加密標準 d e s 算法的安全性是基于有限域上計算離散對數(shù)的困難性 然而 隨著密碼分析技術的發(fā)展 d e s 面臨巨大的威脅 1 9 9 7 年4 月 美國國 家標準和技術研究所 n i s t 發(fā)起了征集a e s 算法的活動 目的是確定一個公開 的 全球免費使用的加密算法 用于保護敏感信息 成為新的數(shù)據(jù)加密標準 2 0 0 0 年1o 月 比利時密碼專家j o a nd a e m e n 和v i n c e n tr i j m e n 推薦的r i j n d a e l 算法被 選擇位a e s 算法 在不久的將來可能會取代d e s 被廣泛使用 對稱密碼體制的最大優(yōu)勢是加密解密速度快 適合于對大量數(shù)據(jù)進行加密 但是對稱密碼技術要求通信雙方事先交換密鑰 如果任意兩個用戶通信時都使用 互不相同的密鑰 則n 個人就要使用n n 1 2 個密鑰 使得密鑰的管理 密鑰 產(chǎn)生 分發(fā) 更換等 非常困難 當系統(tǒng)用戶多時 例如在網(wǎng)上購物的環(huán)境中 商家需要與成千上萬的購物者進行交易 若采用對稱密鑰加密技術 商家就需要 管理成千上萬的密鑰與不同的對象通信 除了存儲開銷外 密鑰管理是 個幾乎 不可能解決的問題 另外 雙方交換 更新密鑰時 密鑰在傳遞過程中容易泄漏 威脅著系統(tǒng)的安全性 南京郵電學院碩士學位論文 2 1 3 非對稱密碼體制 非對稱密碼體制又稱雙鑰或公鑰密碼體制 是密碼學方面的一個巨大進步 1 9 7 6 年d i f f i e 和h e l l m a n 以及m e r k l e 分別提出了非對稱密碼體制的思想 它需 要使用一對密鑰來分別完成加密和解密操作 一個公開發(fā)布 稱為公開密鑰 f p u b l i ck e y 另一個由用戶自己秘密保存 稱為私有密鑰 p r i v a t ek e y 這兩個 密鑰相互關聯(lián) 卻又截然不同 知道其中的一個密鑰并不能推導或計算出另一個 密鑰 在運算上是不可能的 信息發(fā)送者用公開密鑰去加密 而信息的接收者 則用私有密鑰去解密 其基本思想如圖2 3 所示 通過數(shù)學的手段保證加密過程 是一個不可逆過程 即用公鑰加密的信息只能用與該公鑰配對的私鑰才能解密 反之亦然 圖2 3 非對稱密碼體制 非對稱密碼算法主要有r s a e 1 g a m a l p k c s p g p r a b i n m c e l i e c e 等 其中最常用的是r s a 算法 它的安全性是基于數(shù)論中大整數(shù)分解的困難性 其 公鑰和私鑰是一對大素數(shù)的函數(shù) 要提高安全性 就要采用盡可能大的整數(shù) 系 統(tǒng)的加密和解密速度則取決于大整數(shù)的模指數(shù)運算 近年來 橢圓曲線密碼體制 e c c 成為研究熱點 其安全性是基于定義在橢圓曲線點群上的離散對數(shù)問題的 難解性 與其它非對稱密碼算法相比 e c c 能提供更好的加密強度 更快的執(zhí) 行速度和更小的密鑰長度 在密碼學界被普遍認為有可能代替r s a 算法而成為 通用的非對稱密碼算法 但是 e c c 算法本身還有待進一步的研究 非對稱密碼體制的保密性比較好 機制靈活 消除了最終用戶交換密鑰的需 要 解決了密鑰的管理和發(fā)布的問題 是目前商業(yè)密碼的核心 商家可以公開其 公鑰 保留其私鑰 客戶就可以用商家的公鑰對發(fā)送的信息進行加密 安全的傳 送到商家 然后由商家用自己的私鑰進行解密 此外 非對稱密碼技術還使得通 信雙方可以安全地確認對方身份和公開密鑰 提供通信的可鑒別性 因此非對稱 1 6 南京郵電學院碩七學位論文 密碼體制的