基于StrandSpace模型的安全協(xié)議形式化分析研究.pdf

西南交通大學 碩士學位論文 基于Strand Space模型的安全協(xié)議形式化分析研究 姓名 程娜 申請學位級別 碩士 專業(yè) 密碼學 指導教師 何大可 20060501 西南交通大學碩士研究生學位論文 第1 頁 摘要 隨著網(wǎng)絡的普及以及電子商務和電子政務的蓬勃興起 網(wǎng)絡安全問題曰 顯突出 安全協(xié)議 作為解決安全問題最行之有效的方法 也就變得越來越 重要 然而 在復雜的網(wǎng)絡環(huán)境中 要確保安全協(xié)議的正確睦卻是件很難解 決的問題 它已成為一項重要的研究課題 2 0 年來 為了應對這一挑戰(zhàn) 科 學家們在安全協(xié)議分析這一領域投入了大量的精力 在已有的理論和方法中 形式化分析方法的成果較為突出 在各種形式化分析方法中 被普遍認為最有前景的晶新研究成果是由 F a b r e g a H e r z o g 和G u n m 孤三人提出的S 汀a n dS p a c e 模型 它充分吸收了前 人的研究成果 使用一種節(jié)點問存在因果關系的有向圖來表示協(xié)議中主體 入侵者的動作序列 利用證明的方法推導協(xié)議的正確性 可以防止狀態(tài)空間 爆炸 它是一種直觀 簡潔 嚴格 有效的形式化分析方法 本文深入研究了s 圩a n ds p a c e 理論 并用該理論分析了若干協(xié)議 l Y a h a l o m 協(xié)議 建立了Y a h a l o m 協(xié)議的s t r a n ds p a c e 模型 并進行了 深入的討論 2 一種傳輸模型的認證協(xié)議 建立了該協(xié)議的S t r a n ds p a c e 模型 通過 分析 發(fā)現(xiàn)協(xié)議存在漏洞 并構造出了一種攻擊方法 最后針對漏洞對協(xié)議 進行了改進 3 I s l 支付協(xié)議 將S 訂 d s p a c e 理論運用到電子商務協(xié)議公平性的分析 中 得到了與其他分析方法一致的結果 此外 本文在基礎理論部分對代理多重簽名進行了研究 提出了一種增 強的代理多重簽名方案 關鍵詞 安全協(xié)議 形式化分析 s t r a n ds p a c e 模型 公平性 代理多重簽名 西南交通大學碩士研究生學位論文 第1 I 頁 A b s t r a c t W i t ht h ep o p u l a n z a I i o no fn e 研 止肌dI n t e m e ta p p l i c a t i o n s s e c u r l I yi s s u e s a r eb e c o m i n gm o r ea 1 1 dm o r ei m p o r t a n tA c c o r d i g l y s e c u r i t y p r o t o c o l t h em o s t e f f e c t i v ew a yt os o I v es e c u r i t yi s B u e s i so ft h es a I l l ei m p o r t 肌c eB u t i sn o ta n e a s yw o r kt oe n s u r ct h ev a l i d i t yo fs e c u f n yp r o t o c 0 1i nt h es o p h i s t i c a t e dn e l w o r k e n v i r o n m e n l w h i c hh a sb e c o m ea ni m p o n a n tr e s e a r c hs u b j e c tG T e a te f f b r t sh a v e b e e nm a d eb ys c i e n t i s t st om e It l l i sc h a l l e n g ed 嘶n gt h ep a s I2 0y e a r s w h i c hi n as e n s es h o w s 1 l ed i m c u l t yo fs e c u r i t yp r o t o c 0 1 sa n a l y s i s A m o n ga 1 1e X i s t m g t h e o r i e sa n dm e c h o d s f b m a la I l a l y s i si sa no u t s t a l l d i n go n e T h eu p d a I e dr e s e a r c hf h l i t S t r a n ds p a c eM o d e l S S M b r o u g h tf o r w a r db y F a b r e g a H e r z o ga I l dG u l t n l a ni so ft h eb e 8 tp r o s p e c ta m o n gv a d e t i e so ff o m l a l a 1 1 a l y s i sm e m o d sa tl a 唱e I tf u l l ya b s o r b sf o m l e rr e 8 e a r c h i n gr e s u l t sa n du s e sa k i n do fo r d e rg r a p hb e t V e e ni t sn o d e se x i i n gc a s u a lr e l a t i o n s h i pt od e m o n s t r a t e m ea c t i o ns e q u e n c eo fm a i nb o d ya n di n t r u d 盯o f 出ep r o t o c 0 1a n dd e d u c em e V a l i d i t yo ft h ep r o t o c 0 1b ym e 鋤8o fc e r t i 6 c a t i o n nc a I lp r e v e n tt h eb u r 8 t i n go f s t a t u ss p a c ea n di sp r a c t i c a l i m u n i V ea n ds t 打c tf o rf 0 皿a l 肌a l y s i so fs e c u 打t y p m t o c 0 1 T h i sp a p e rd o c saf I l r t h e rs n l d yo nt h eS S M 缸dt h e na n a l e sn u r n b e f so f s e c u r i t yp r o t o c o l sb a s e do n i ta sf 0 1 l o w s 1 Y 她a l o p m t o c 0 1 E s t a b l i s ht h eS S Mo f m a l o m p r o t o c o I a n dc o n d u c tt h ef L l I t l l e rd j s c u s s i o n 2 A 妯I l do fa u t h n c a t i o np r o t o c 0 1b a s 亡do n at r a I l s m i s s i o nm o d e l w i t hS S M w e f i n do u tn sd r o p p e r 觸dc r e a t ca n e wa t t a c ko n t h i sp r o t o c o l a n dm a k es 岫ei m p m v e m 髓t 3 I S lp a 腳e mp r O t O c 0 1 w e 印p l y m eS S M t o t h e 蛆a l y s i so f 蜘m e s so f E b u s i n e s sp r o t o c o l A d d i t i o a l l y w es t u d yo p r o x ym u l t i s i 9 1 1 a m r es c h e m ei nb a s i ct h e o r ya 士1 d p r c s 叨tas t r e n g t h e n e dp r o x ym u l t i s i g n a t u r es c h e m e 西南交通大學碩士研究生學位論文第1 I I 頁 K e yw o r d S e c u r i t yp r o t o c 0 1 F o r m a la n a l y s l s S t r a n dS p a c eM o d e l F a i m e s s P r o x ym u l t i s i g n a t u r e 西南交通大學碩士研究生學位論文 第1 頁 1 1 研究背景 第1 章緒論 計算機網(wǎng)絡正以驚人的速度向各個領域滲透 成為各領域發(fā)展的新源泉 各種現(xiàn)實世界里的組織與系統(tǒng)正在走進網(wǎng)絡這個虛擬的世界 使網(wǎng)絡世界變 得更加精彩 與此同時 安全問題也變得日益突出 復雜 解決安全問題對 許多網(wǎng)絡應用來說已是頭等大事 從目前解決安全問題的方式來看 安全協(xié) 議是最有效的手段之一 它可以有效地解決以下一些重要的安全問題 源認 證和目標認證 消息的完整性 匿名通信 抗拒絕服務 抗抵賴 授權等 另一方面 隨著網(wǎng)絡技術的飛速發(fā)展 多播技術已不斷走向成熟 由多播應 用帶動的安全問題也變得更加復雜 為解決這些問題也是通過一種稱為群協(xié) 議的安全協(xié)議來完成的 目前研究熟點之一的多主體系統(tǒng)中的安全主體問題 在很大程度上也是依靠有效的安全協(xié)議的設計來完成的 可見 安全協(xié)議是 一個十分重要的研究課題 在一個分布式的互聯(lián)網(wǎng)網(wǎng)絡環(huán)境中 人們通過安全協(xié)議來具體實現(xiàn)安全 共享網(wǎng)絡資源的需求 然而 安全協(xié)議的設計極易出錯 而且十分困難 即 使我們只討論安全協(xié)議中最基本的認證協(xié)議 其中參加協(xié)議的主體只有兩三 個 變換的消息只有3 5 條 設計一個正確的 符合認證目標的 沒有冗余 的認證協(xié)議也十分困難 正如實際應用中已有的安全協(xié)議往往被證實并不如 它們設計者期望的那樣安全 復雜而惡意的網(wǎng)絡環(huán)境使得攻擊者可利用安全 協(xié)議自身的缺陷來實施各種各樣的攻擊 從而達到破壞網(wǎng)絡的目的 即使一 個安全協(xié)議被很小心仔細地設計了 并被使用了很多年 仍然包含一些微妙 的漏洞沒有被發(fā)現(xiàn) 設計一個符合安全目標的協(xié)議 僅僅知道系統(tǒng)的安全需 求遠遠不夠 我們需要確保所設計的協(xié)議在系統(tǒng)參與的各方之間能夠運行良 好 因此 安全協(xié)議的安全性成為網(wǎng)絡安全的關鍵 考量和分析一個安全協(xié)議的安全性 我們稱之為安全協(xié)議的分析 二十 多年來為了應對這一挑戰(zhàn) 科學家們投入了大量的精力設計開發(fā)了不同種類 的研究理論與方法 比如形式化方法 可證明安全理論 零知識證明理論等 西南交通大學碩士研究生學位論文 饕2 頁 形式化分析就是將安全協(xié)議及其所處的環(huán)境視為一個系統(tǒng) 運用各種正規(guī)的 模型化的 標準的 客觀的方法 這魑方法可以是理論推證 也可以是工程 技術實現(xiàn) 可以是擠議分析專制的 齙可以是般目豹性的 雍驗證安全協(xié) 議的說鹱是否能夠達成箕疆期的目標 安全協(xié)議形式化分撬從8 9 年起至今 凡年的辯赫量發(fā)展搬為迅速 目 前已成為安全執(zhí)議研究領域一個極為重要 頗具理論深度 同時也是任何人 無法回避的 個前沿課題 1 2 論文的研究意義 安全協(xié)議的形式純分轎研究已取得了許多顯著的成栗 其中具有代表性 的就是著名的D o l c v Y a o 模型1 1 和B A N 邏輯 但是安全協(xié)議的研究也同樣 掰臨臣大挑戰(zhàn) 是一件復雜 困難的工作 安全協(xié)議的研窺存在最大的 個 稠惑就是 被證明不正確的安全執(zhí)議肯定有漏灝 但被證明為正確豹安全協(xié) 議卻不能保 芷沒有漏洞 導致上述目題的原因是多方西靜 蘺先 安全目標 本身十分微妙 也不確定 例如 關于認證性的定義 至今存在各種不同的 觀點 其次 安全協(xié)議運行環(huán)境非常復雜 攻擊者無對無判不存在 手段和 能力無法獒捧1 鑫計和量化 刻畫安全協(xié)議的運行環(huán)境和形式億描述裴擊者的 能力都是艱巨的任務 最后 安全協(xié)議的運行是不確寇的 因為它們其有高 并發(fā)性 強前 在安全協(xié)議形式化分析領域最毒菌景的方向就跫結含采用模型檢 測技術和定理證明方法開發(fā)分析拇議的自動驗證工具 嗣翦已取得了一些研 究成果 F D R M u T c p 4 1 h l t e r r o g a t o r c 5 均B n l t u s 6 1 自動驗證工具的優(yōu)勢 在于荔用性和實用性 但缺點在于容易受到狀態(tài)空間嚴重爆炸問題的困擾 這使樗它們不能分析一蝗大型復雜的協(xié)議 s t 煳ds p a c e 模型由F 曲r e g a H e r z o g 和e I u t I n a n 三人于1 9 9 8 年提出 7 s 訂a n ds p a o e 模型溝提出為解決安全協(xié)議設計與分拆的豳難提供了一種霹能 該方法吸納了N R L 協(xié)議分析器 S c h n e i d e r 秩函數(shù)和p a u l s o n 歸納法等思怒 口I 它是現(xiàn)有安全掩議形式佬方法中精為直攫 鏑沽 嚴格稀有效的方法 它充分吸收了前人的研究工作成果 它的喜觀性表現(xiàn)在使用一種節(jié)點闖存在 因果關系的有向圖來表示協(xié)議的運行 它的簡潔牲表現(xiàn)在對予小型協(xié)議完全 可以使用手工的方法完成證明 它的嚴格性表現(xiàn)在它使艏了節(jié)點之闖的因果 誣南交通大學顴士研究生學位論文第3 頁 關系來確保證明的邏輯性和證明的正確性 它的有效性可以通過文獻 7 9 1 0 中繪出的實例來說明 利用S 蟣m dS p a c e 理論分析安全協(xié)議的安全性己經(jīng)取 得了很多成巢 在理論研究和工其開發(fā)方面都壽新鼢進展 C H v e s a t o D u r g i n K a n o v i c h 和s c e d r o v 使用線形邏輯對S t r a n ds p a c e 進行解釋 s e r s o n 使 用s 訂a n dS p a c e 的語義襲現(xiàn)認證性邏輯叫 另外 D s o n g 對s t r a n ds p a c e 模 型進行了擴充 j 入了S t r a n ds p a c e 中番要索的語法和語義 并對安全游 議韻認證性進行了邏輯的表示 在此基礎上又使用S M L 語言開發(fā)了一個安 全協(xié)議自動驗證工具A T H E N A 實現(xiàn)了對認證性安全協(xié)議的自動驗證 但該工 具對秘密憔協(xié)議的證明是不完善的 綜 t 所述 對s 打a n ds p a c e 模型的研究應嗣既宥理論意義也有現(xiàn)實意義 1 3 論文的主要工作及組織結構 論文菇分為五章 主要工作涉及基礎理論研究和基于S l r a n ds 口a c e 模型 的安全協(xié)議分析研究兩犬部分 具體安排如下 第一章 緒論 介縉了論文的研究背景 意義及總體框架 第二章 基礎理論研究 介紹丁安全協(xié)議形式化分析的密碼學理論基礎 介紹了數(shù)字簽名技術及 公鑰體制 提出了一種增強的代理多重簽名方案 第三章 安全協(xié)議形式化分析綜述 介紹了安全協(xié)議的定義 分類 性質 設計原則及可能存在的缺陷類型 概述了安全晦議形式化分板的歷史 研究現(xiàn)狀 分類 第四章 s 咖m dS p a c e 理論與模型 介紹了s l r m dS p a c e 理論與模型 定義了一些基本概念 給出一些命題 l 理和定理以及相關的證明 指措了S 細刪s p 8 c e 模型的優(yōu)點及不足 第五章 若干密碼瓤議的s 仕a n ds p a c e 模型及分析 介紹了N S L 協(xié)議的S 打a 1 1 d S p a c e 模型及分析 構造了詘a I o m 協(xié)議的 s 扛鑫n dS p a c e 模型并對其進行了分析 運用s 打孤ds p e 模型對一種傳輸模型 的認證協(xié)議進行了分析并發(fā)現(xiàn)了漏洞 給出了一種攻擊 并對協(xié)議進行了改 進 將s l m n ds p a c e 模型運用于安全協(xié)議的公平性分析 分析了l S l 支付協(xié)議 蓖審交通大學碩 研究生學位論文第4 頁 的公平性 得到了其他分析方法相同的結論 結論 總結了本論文的主要工作 對以后工作進行了展望 最后是參考文獻 致謝以及玫讀學位期問發(fā)表和即將發(fā)表的論文 西南交通大學碩士研究生學位論文第5 頁 21 密碼學簡介 第2 童基礎理論研究 密碼學是網(wǎng)絡信息安全科學和技術研究最為直接的基礎學科 是保證信 息安全的關鍵技術 密碼學 源于希臘語 英文為c r y p t o g o r a p h y 有著漫長 豐富的歷史 它研究如何把信息轉換成一種隱蔽的方式 阻止其他人理解獲 得 在過去 密碼學用于重要的交流活動中 如間諜活動和反間諜活動之間 或外交官和總部聯(lián)系之間等 密碼學方法分為兩類 一類叫隱寫術 s t e g a n o g r 印h y 另一類叫密碼編碼學 前者是將秘密信息隱藏在大量無用 的信息當中 信息的冗余度較大 后者是通過各種文本轉換的方法使得信息 為外部不可理解 本文所涉及到的密碼學是指密碼編碼學 以下稱為密碼學 現(xiàn)代密碼學是一門跨多學科 涉及理論 工程面廣的復合型科學 它可 以被看作是信恩論理論 使用了大量的數(shù)學領域的工具 如眾所周知的數(shù)論 和有限域知識 密碼學也可以說是工程學的一個分支 不同的是它必須應對 一些活動頻繁 高度智慧 懷有惡意的敵人的攻擊 早期的密碼學采用兩種 方法 把給定信息的字母打亂順序進彳亍重排 或者使用一組字母替換另一組 字母 如著名的愷撒密碼和H i l l 密碼 進行這種操作需要一個密碼本 c o d e b o o k 現(xiàn)代的密碼學 由于使用了計算機對信息進行處理 所以與傳統(tǒng)的密 碼編碼學有了很大的不同 操作的對象從以前的字母或者文字變成了計算機 內部表示的0 l 序列 通信雙方進行交互傳遞的信息也不再是字母或者文字 而是可以被計算機理解的O l 序列 近幾十年來 隨著計算機和網(wǎng)絡的普及 密碼學取得了驚人進展 它的使用范圍和功能越來越廣 從保密性和認證性 擴充到了匿名性 不可否認性等等 2 2 密碼體制 密碼體制是信息安全的基石 原始的未被處理過的信息 稱為明文 p l a i n t e x t 被保護后的明文 稱為密文 c i p h e r t t 將明文轉換成密文 p l a i n I e x t 被保護后的明文 稱為密文 c i p h e r t t 將明文轉換成密文 西南交通大學碩士研究生學位論文 第6 頁 這一過程稱為加密 e I l c r y p t i o n e n c i p h e r i n g 操作 反之稱為解密 d e c r y p t i o n d e c i p h e r i n g 揉作 加 解密操作中所使用的類似于鑰匙的額外附加信息 分蹦穗為由睡密密鑰 解密密鑰 把明文加密成密文的具體步鞭秘方法 稱為 加密算法 反之稱為解密算法 般而言 加解密算法是公開的 而保密性 是基于對密鑰訪問的約束 加 解密算怯的有機結臺構成了鬻碼體制 密碼 體制分為積鑰密碼體制和公鑰密碼體制 1 私鑰密碼體制 加密密鑰和解密密鑰是相同的 或者兩者之間容易互相導出的密碼體制 稱為私鑰密碼體制 也稱為對稱密碼體制 在這種系統(tǒng)中 加密密鑰或者解 密密鑰暴露將會使得整個加密饞制被攻破 囂此 私鑰系統(tǒng)密碼的一個嚴熏 缺陷就是在任何密文傳輸之前 會話通信的雙方必須使用一個嚴格安全的倍 道預先協(xié)商加 解密密鑰 在實際巾 達到這一點是很難的 在私鑰密碼體 制中 使用最為廣泛也最為著名的就是2 0 世紀8 0 年代公布的數(shù)據(jù)加密標準 D E s D a t aE n c r y p t i o nS l a l l d a r d 和2 0 0 0 年公布的高級加密標準A B S A d v 姐c e dB n c r y p t i o ns t a l l d a r d 私鑰密碼體制的優(yōu)點在于速度快 硬件蜜 現(xiàn)比較容易 因為大部分的操作都是邏輯和羲換 在現(xiàn)實生活中 銀行的A T M 機一般都使用D E S 加密體制 2 公鑰密碼體制 加密密鑰和解密密鑰是不同的 且兩者之同難于互相推導的密碼體制 稚為公镅密碼體讎 也稱為非對稱密碼體制 公鑰密碼體制氍可用于加密又 可用于數(shù)字簽名 數(shù)字簽名可以為每個人確定一個身份 而不需要使用傳統(tǒng) 的手工簽名等方法來鑒別和證明身份 這是公鑰密碼體制的一個偉大創(chuàng)新 公鑰密碼體制的思想提出以后 各種算法的加密體制和數(shù)宇簽名方案紛紛出 臺 其中最著名的是由m v e 8 t S h a m r 和A d l e m a n 在1 9 7 8 年攝池的R S A 體 制 l R S A 體制是一種基于數(shù)論中大素數(shù)分解的困難性的公鑰密碼體制 是 歷史最悠久 應用最廣泛的公鑰密碼體制 另外就是基于離散對數(shù)求逆困雉 性聞題建立起來的班G a I n 3 l 體制和橢強曲線密鸚體銣 E C C 公鑰密碼體 制的優(yōu)點在于安全性和應用廣泛性 但缺點是運弊速度太慢 不適舍直接用 于對原始信息的加密和簽名 在現(xiàn)蟲中 公鑰密碼體制的應用已經(jīng)十分非常 廣泛 如P E M P 五v a c y B m a n c e d M a n S M n 姬 P G p X 5 0 9 等 綜合私鑰密碼體制和公鋸密碼體制各自的優(yōu)缺點 在密碼學的解決方案 中經(jīng)常使用公鑰密碼體制來保護私鑰密碼體制中所使用到的加密密鑰 如 誣南交退大學磧士磅究生學位論文第7 頁 D i m e H e l l m a l l 密鑰交換算法 而在簽名的解決方案中則引進了H a s h 函數(shù) 只對簽名信息的H a 盎結聚 犀定躍度的信息 稱為消息摘要 進行簽名操 作 2 3 數(shù)字簽名 2 3 l 數(shù)字簽名技術 個數(shù)字簽名方案至少應滿足以下三三個條件 1 簽名者事后不能瓚認自己的簽名 而任何其他人都不能偽造簽名 2 接受者能驗證簽名 3 當雙方關于簽名的真?zhèn)伟l(fā)生爭執(zhí)時 第三方能解決雙方之間發(fā)生的 爭執(zhí) 根據(jù)數(shù)字簽名標準D s s 數(shù)字簽名的步驟一般森以下幾步 步驟l 發(fā)送方用一個H a s h 函數(shù) 如s 臥 1 或M D 5 算法 對消息進行 處理 彤成一個固定長度的消息摘要m 步驟2 發(fā)送方用自己的私鑰對消息摘要 進行數(shù)字簽名計籜 生成數(shù) 字簽名 步驟3 將數(shù)字簽名和原始消息一起發(fā)送給接收方 步驟4 接收方用同樣的H a s h 函數(shù)侔用予接收到的原娘消息 生成消惠 摘要m 2 步驟5 接收方用發(fā)送方的公鑰解密數(shù)字艇名得到消息摘要m 與消 息摘要 2 對比 二者相同則通過該數(shù)字簽名的驗證 否則該數(shù)字簽名驗證失 敗 2 3 2 數(shù)字簽名技術與如密技術的縮合 在實際應用中 如果信息是公開螅 僅要求不可偽造 如喇頁信息 則 可利用數(shù)字簽名技術來保證信息的完整性和不可偽造性 如果信息是傈密的 如E m a 弧電子商務等 則不儀要保證其完整性 還要保證其秘密性 此 時需要信息加密技術與數(shù)字簽名技術同時使用 一般工作過程如下 發(fā)送方一 1 形成發(fā)送消息P 的消息摘要M 并用私鑰對此接耍加密生成C 鋤 2 將消息P 與c m 一起用對稱密鑰加密生成o 西南交通大學碩士研究生學位論文 第8 頁 3 用接收方四的公鑰加密對稱密鑰生成c b 4 將C p 和c 一起發(fā)送給接收方口 接收方B 接收到消息后 1 用私鑰解密c 得到對稱密鑰 2 用對稱密鑰解密c b 得到消息尸和加密后的摘要C M 3 用同樣的H a s h 函數(shù)生成消息P 的摘要 l7 并用發(fā)送方一的公鑰解 密西l 得到腳 比對肌和m7 若二者相等則說明消息P 正確 2 3 3 一種增強的代理多重數(shù)字簽名方案 1 基本柵念 1 代理簽名 1 在一個代理簽名方案中 一個被指定的代理簽名者可 以代表原始簽名者生成有效的簽名 2 多重代理簽名 在一個多重代理簽名方案中 多個原始簽名人分 別將簽名權委托給各自的代理簽名者 多個代理簽名者可以代表各自的原始 簽名者生成有效的簽名 3 代理多重簽名 1 q 在一個代理多重簽名方案中 多個原始簽名人將 各自的簽名權委托給同一個代理簽名者 此代理簽名者可以同時代表多個原 始簽名者生成有效的簽名 2 Q i 和H a r n 的代理多重數(shù)字簽名方案 安全參數(shù) 口 q 為大素數(shù) 且q I p 1 g 乙 是一個g 階元 是一 個安全的H a s h 函數(shù) 設A 是若干原始簽名人 曰為代理簽名人 其身份標 識號分別為 z 每一位原始簽名人和代理簽名人的私鑰分別為 z f x 日E 1 P l 公鑰為 g m o d p 口 g 如m o d p 授權過程 設m 為待簽名的消息 1 每個 隨機選取女 l p 1 并計算岸 g n l o d p 公丌足 從 而每個 都可以計算 K K 腳d p q 麟I j t m o d 口0 1 厶 月 f 1 4 i 送代理子密鑰 s 皿 給胃 2 曰取得 足 s z 后驗證授權方程 g K M m o d p 2 1 如果 2 1 式成立 接收 世 s D 否則艷絕騷收 Kr J sJ 簽名過程 占選取隨機數(shù)f 1 p 1 并計算 s s x m o d F J s m o d q y m o d p b l y 兀兒m o d p J t l s 作為代理簽名的密鑰 B 送 v z D 丘 m 給簽名驗證者 代理簽名驗證過程 r 接收到 v z m 后 計算彭 n Kr n o d P 兒 丌 i m o d p 并驗 i lI l 證驗證方程 y 培a 1p m o d p 2 2 如果 2 2 式成立 y 接收 v 佃 m 否則拒絕接收 V m 3 w a n g 和F u 構造的偽造攻擊及其方案改進1 1 8 設n 個原始簽名人中也企圖偽造一個有效的代理多重簽名 一 作如下操 作 1 A 隨機選取 1 p l 并計算 M 兒4n 一m o o m 世 y j n 掣m o d p 產1 J I 3 l t J 并公晦y 是他的公鎮(zhèn) 其呻yJ y 2 y y I j h 是A A2 A 爿H A 的公鑰 2 隨機選取f 1 p 1 1 并計算 K n K f m o H d p m o d p V c 工 碰 M 州 m 0 H d q 假冒丑送偽造的簽名數(shù)據(jù) v 上D 啪給簽名驗證者y 3 礦接收到 v 礬 m 后 計算足 n K m o o 弘兒 兀y m o d p r z l 并驗證驗證方程 2 2 式 偽造的 u D 口 m 能使 2 2 式成立 其原因為 H y l J H y 丌y j l m o d y 1 y m o d p 西南交通大學碩士研究生學位論文第l o 頁 K K H 世 丌茁廣m o d p 丘川 K y m o d p I l 1 I y y y 雪弛y 尹 枷 2 y 筍 世 伽 m o d 則 2 2 式成立 因此 偽造的簽名0 v D m 能通過驗證方稗的驗證 為了避免上述偽造攻擊 文獻 1 8 對文獻 1 7 方案進行了改進 增加一個 代理簽名管理中心c A 由C A 對原始簽名人的公鑰進行驗證 避免了原始 簽名人可能的偽造攻擊 限于篇幅考慮 該改進方案在此不再贅述 4 改進的代理多重數(shù)字簽名方案 在Q i 和H a r n 的方案中 偽造攻擊有效的主要原因是在驗證方程中可求 出表達式 乃 兀y 女 兀蚋 I t 1 盧f 使得 J K y 就可以避開驗證方程中所包含的代理簽名人的私有信息 通過驗證 根據(jù)以上分析 本文提出的改進方案如下 安全參數(shù) P g 為大素數(shù) 且目l p 1 呂 乙 是一個g 階元 是 一個安全的H a s h 函數(shù) 設也是若干原始簽名人 曰為代理簽名人 其私鑰 分別為一 z 口 1 p 1 公鑰分別為y g m o d p 兒 g hr n o d p 公開 委任狀w j 是 將簽名權利委托給曰的文件 它明確了一 與口之間的代理關 系 w f 4 m B r 叩e e t c 其中國 上D 是 哇 的身份 工D 口是B 的 身份 F 是授權證書的有效期 叩F 是授權范圍 s 把是其他的相關參數(shù) 授權過程 設m 為待簽名的消息 1 每個一i 隨機選取女 1 p 1 并計算 世f 窖 r n o d p q y J 足 七f z P m o d g 1 1 2 一 送代理子密鑰 置 J 給口 2 占取得 墨 J w f 后驗證授權方程 g l J x J m o d 蘆 2 3 如果 2 3 式成立 接收 墨 5 H 否則拒絕接收C 巧 s 簽名過程 曰選取隨機數(shù)f 1 p 1 并記錄時間戳霸 之后計算 西南交通大學碩士研究生學位論文 第l l 頁 J x 芋 J m o d 目 y m o d P V f 幽 矗 m o d 口 f 1 s 作為代理簽名的密鑰 口送代理簽名數(shù)據(jù) D 四 v L 給簽名驗證 者r 代理簽名驗證過程 y 接收到 m j m 后 在原始簽名人公開信息處取得委任 狀 核對m 以及代理簽名人的身份是否在所有委任狀的集畬 w l w 2 H 許可的范圍內 如有任何一條不符 拒絕接收 D u 巧 m 否則 計算口 后驗證驗證方程 兀挺j n y 玎o m o d J 口 2 4 f 司l e l 如 2 4 式成立 礦接收 上D v L 否則拒絕接收 皿 v L m 5 安全性分析與討論 1 攻擊分析 1 由于在授權方程中含有原始簽名人的私有信息 所以任何人不可能 在截取代理子密鑰后冒充原始簽名人A f 進行非法授權 2 由于在驗證方程中包含有所有原始簽名人的私有信息 所以任何人 包括代理簽名人不可能在沒有得到原始簽名人一 合法授權情況下 進行非法 代理 3 反之 原始簽名人A 不可抵賴合法的授權 由于代理簽名及驗證方程中所包含的代理簽名人曰的私有信息z 可以 有效地保證代理簽名由代理簽名八日發(fā)出 如果攻擊者欲偽造簽名來通過驗 證 其計算難度等價于離散對數(shù)的分解難度 所以本方案可有效抵御4 5 4 原始簽名人的合謀攻擊 5 攻擊者截獲代理子密鑰后冒充代理簽名人口偽造代理簽名 6 顯然本方案可有效的抵御文獻 1 8 所提出的偽造攻擊 7 反之代理簽名人口也不能對合法的代理多重數(shù)字簽名進行抵賴 8 由于引入了委任狀 原始簽名人就可對代理簽名人口的簽名能力 進行限制 可以通過 明確曰只能在一定的有效期 一定的范圍內參與多重 簽名 p 不接受超出權限的簽名 一旦超出有效期 代表原始簽名人收回代 理簽名權 這樣 避免了丑濫用簽名權力 對原始簽名人是公平的 西南交通大學碩士研究生學位論文 第1 2 頁 9 由于在代理簽名過程中系統(tǒng)加入了時間戳 可以讓驗證用戶能夠 檢測該簽名的時間信息 有效抵御重復攻擊 2 任何人可驗證代理多重簽名的有效性 因為有 y y 產一吡y 拋刪 黔 P 吡 n 足j n y 臚w 川m o d p 3 無需引入第三方 對整個系統(tǒng)實現(xiàn)而言 減少了不安全因素 通過以上分析可知 新方案是一個增強的代理多重數(shù)字簽名體制 滿足 以下性質 1 可驗證性 任何驗證人都可以驗證代理多重簽名是否有效 根據(jù)有 效的代理多重簽名 確認所有原始簽名人都承認已經(jīng)簽名過的文件 2 強不可偽造性 因為代理多重簽名包含代理簽名人的私有信息 除 了代理簽名人之外的任何其他人都無法偽造代理簽名 3 強身份證實性 因為代理多重簽名中包含代理簽名人的公鑰 任何 人可以從代理簽名中確認參與的代理簽名人身份 4 強不可抵賴性 任何一個原始簽名人和代理簽名人都不能否認一個 由他們參與生成的代理多重簽名 綜上所述 此方案在不引入可信任第三方的前提下 對文獻 1 7 提出的 代理多重數(shù)字簽名方案進行了改進 有效的克服了文獻 1 8 提出的攻擊方法 不但保留了文獻 1 7 的代理多重數(shù)字簽名方案的優(yōu)點 而且在授權時效 范 圍和加入代理簽名的時間信息等方面有所加強 可以更加安全有效地實現(xiàn)由 一個代理簽名人生成代表多個原始簽名人的代理簽名的目的 同時 無需引 入第三方以及驗證方程中無需為求逆而作大量的計算使得本方案更加簡潔實 用 我們認為 這種簽名方案在電子商務和網(wǎng)絡安全通信方面有廣泛的應用 前景 可用于構造具有良好性質的公平交換協(xié)議 電子選取協(xié)議等 西南交通大學碩士研究生學位論文 第1 3 頁 第3 章安全協(xié)議形式化分析方法 計算機剛絡正以驚人的速度向各個領域滲透 碰為各領域發(fā)展的新源泉 各種現(xiàn)實世界里的組織與系統(tǒng)正在走進網(wǎng)絡這個虛擬的世界 使網(wǎng)絡世界變 得更加精彩 與此同時 安全問題也變得日益突出 復雜 解決安全問題對 許多網(wǎng)絡應用來說已是頭等大事 從目前解決安全問題的方式來看 安全協(xié) 議是最有效的手段之一 它可以有效地解決以下一些重要的安全問題 源認 證和目標認證 消息的完整性 匿名通信 抗拒絕服務 抗抵賴 授權等 另一方面 隨著網(wǎng)絡技術的飛速發(fā)展 多播技術已不斷走向成熟 由多播應 用帶動的安全問題也變得更加復雜 為解決這些問題也是通過一種稱為群協(xié) 議的安全協(xié)議來完成的 目前研究熱點之一的多主體系統(tǒng)中的安全主體問題 在很大程度上也是依靠有效的安全協(xié)議的設計來完成的 可見 安全協(xié)議是 一個十分重要的研究課題 盡管安全協(xié)議是保護信息系統(tǒng)安全的有效手段之一 但是安全協(xié)議自身 安全性的分析卻是一個非常困難的問題 目前已經(jīng)有多種研究安全協(xié)議的理 論與方法 如形式化分析方法 可證明安全理論 零知識證明理論等 本章 主要綜述安全協(xié)議形式化分析的理論與方法 為了便于更好地理解這些理論 和方法的應用背景 首先對安全西議的一些基本問題作一簡要概述 3 1 安全協(xié)議 3 1 1 基本概念 1 協(xié)議 協(xié)議是一系列的規(guī)則和協(xié)定 它們被用于定義兩個或兩個以上的參與者 之間的一個通信框架 就是兩個或兩個以上的參與者采取一系列步驟以完成 某項特定的任務 由此可知協(xié)議至少應該具有如下基本性質I 1 1 協(xié)議的參與者不能少于兩個 一個人可以通過執(zhí)行一系列的步驟柬 完成一項任務 但它不構成協(xié)議 2 協(xié)議包含一系列的消息接收和消息發(fā)送行為 參與者還可能會對消 西南交通大學碩士研究生學位論文第 頁 息進行內部處理 3 協(xié)議是有目的的事件 參與各方希望通過執(zhí)行協(xié)議達到一個目的 可能是交流秘密信息 逢可能是確認身穗等 4 協(xié)議的成功依賴于參與各方遵守規(guī)則的參與執(zhí)行 任何一方破壞規(guī) 則都將導致協(xié)議無法順利完成 2 安全協(xié)議 安全協(xié)議也叫密碼安全協(xié)議 或者密碼協(xié)議 就是在消息處理環(huán)節(jié)采用 了若干密碼算怯的協(xié)議 安全協(xié)議運行過程之中的參與卷 稱為主體 這里 孽主體的概念經(jīng)廣泛 可能是入 也可能是一個程序 或者是一個服務器 協(xié)議的運行由一些相互 獨立的有先后順序的動作序列和步驟構成 這種獨立的動作序列被稱為 個 角色或者身份 每個角色的功能是獨立的 但帽瓦之問是關聯(lián)的 交互的 比如發(fā)起者 噙應者等簿 在鑄議中 主體與角色的壤念是不盡相同的 一 個主體可能就代表一個角色 同樣也可能扮演多個角色和身份 從發(fā)起者發(fā) 起一個協(xié)議開始 到雖終協(xié)議的結束 稱為協(xié)議的一輪運行 一輪協(xié)議的運 行當中所涉及到的參與者的數(shù)目 或者角色不一定恰好 睪合安全協(xié)議的規(guī)定 其中那些破壞協(xié)議的正常運行 或者不遵守協(xié)議規(guī)定步驟的參與者稱為攻擊 者 或者叫做攻擊者角色 其他的參與者稱為誠實參與者 或者叫做誠實角 色 協(xié)議的一個參與者蓋 這里也可以使用主體或者角色代替 向另外 一個 參與者口 這里也可以使用主體或者角色代替 傳遞一個消息 稱一的動作 為發(fā)送 口的動作為接收 稱為消息的發(fā)送者 B 稱為消息的接收者 一 個安全協(xié)議p 在運行過程中 假如有攻擊者 攻擊角色 存在 并且沒有被 系統(tǒng)或者誠實角色新察覺 同時攻擊者在參與過程之巾并沒鴦利用飪簿密碼 學上的漏洞 稱安全協(xié)議P 被攻破 即安全協(xié)議P 存在設計上的漏洞 3 安全協(xié)議與算法的區(qū)別和聯(lián)系 協(xié)議與算法的概念楚不盡相同的 算法應用于漭議中清惠處理馳環(huán)節(jié) 協(xié)議對不同的消息處理方式則要求用不同的算法 而對算法的具體化則可定 義出不同的協(xié)議類型 由此可見 密碼算法和安全協(xié)議處于網(wǎng)絡安全體系的 不同層次 是網(wǎng)絡數(shù)據(jù)安全的兩個主要內容 具體而言 密碼算法為網(wǎng)絡上 傳遞瓣消息提供高強度的加解密操作和其飽輔勒算法 如H a s h 函數(shù) 麗安 全協(xié)議是在密碼算法的基礎上 為各種網(wǎng)絡安全性方面的需求提供實現(xiàn)方案 西南交通大學碩士研究生學位論文 第1 5 頁 安全協(xié)議是一門跨領域 跨學科曲科目 涉及剖誑多領域的知識 密碼 學是安全協(xié)議的學科基礎 如果密硒體制被破解則安全協(xié)議將會隨之被破解 褥變得毫無意義 一般情況下我們認為在安全協(xié)議中使用的加密算法足安全 的 不會被破解的 加密算法對于安全協(xié)議而言被看作是一個黑盒予 它提 供對通信協(xié)議信息處理環(huán)節(jié)的加密解密操作 現(xiàn)實的網(wǎng)絡提供安全協(xié)議運行 所需要的環(huán)境 然而 網(wǎng)絡的不穩(wěn)定和不可靠 或者羝質麓又會影響安全協(xié) 波l l 勻實際使用效果 安全協(xié)議是一f 藝術的科學 設計安全協(xié)議絕非簡單的 工作 它需要精確的和復縶的科學思維 安全協(xié)議涉及大量數(shù)學銹域的知識 安全協(xié)議目標的精確和標準的定義必須要借助于數(shù)學語言的描述和刻畫 對 安全協(xié)議的形式化分捱同樣必須借助數(shù)學的模型和手段 安全協(xié)議也可班看 作是一門工程的科學 下同的是它必須虛對一魑活動頻繁的 高度智慧的 懷有惡意的敵人的攻擊 我 所指的攻擊不是針對密碼學體制的攻擊 而是 針對安全協(xié)議設討 本身漏洞的發(fā)現(xiàn)和查找 4 安全協(xié)議的功能 隧著網(wǎng)絡的高度發(fā)展和普及娃及電子商務和電子政務的蓬勃興起 安壘 協(xié)議的作用變樗越來越重要 功能變得越來越強大 早期的安全協(xié)議的匿標 主要是兩個方面 即信息的保密性窩身份的試證性 保密的茸的是防止桃密 信息在傳送過程中被對手破洋 保密性常常被用于傳遞秘密信患的事務當中 認證的目的有兩個 一是驗證信息的發(fā)送者是確定的和翼正的 而不是未知 的 假冒的 二趄驗證信息的完箍性 在信息的傳送或存儲過程中來被篡改 重放或延遲等 在許多情況下 認證性協(xié)議都包臺著保密性的附加目標 即 在主體之闋安全地分配密鑰或其他各種秘密 諷證性常被用于網(wǎng)絡上的身份 識別事務當中 現(xiàn)在的安全協(xié)議的目標已經(jīng)多種多樣 比如 非否認牲 匿 名性和公平性等 非否認性隱含兩層意思 一個是倍患發(fā)送方的非番認性 n o n r c p H d i 醛i o no f o n g i n 即菲否認協(xié)議囪接收方提供不可抵贛的謹據(jù) 證明收到消患的來源的可靠性 另一個是信患接收方的非嚳認 n o n e p n d o no f r e c e i p t 即非甭認協(xié)議向發(fā)送方提供不可抵賴的證據(jù) 證明接收方已收到了某條消息 非否認性常被用于電子簽名和電子政務活動 當中 匿名的露的是確保參與嚳在參與協(xié)議的過程中不泄囂任何有關自己身 份和其他方面的信息 匿名性常被用于電子交易和電子商務活動當中 公平 的目的在于確保協(xié)議參與備方的地位和休用平等 參與各方所擁有的能力逝 是棚嗣的 公平性常被用于屯予選舉和電子投票攀務整中 西南交通大學碩士研究生學位論文篷塑 5 安全協(xié)議的分類 在網(wǎng)絡通信中最常用的 昂基本的安全協(xié)議按照其目的可以分成以下4 類 1 密鑰交換協(xié)議 這類協(xié)議用于完成會話密鑰的建立 一般情況 F 是 在參與協(xié)議的2 個或者多個實體之間建立共享的秘密 如用于1 次通信中的 會話密鑰 協(xié)議中的密碼算法可采用對稱密碼體制 也可以采黼菲對稱密碼 體制 2 認證協(xié)議 認證協(xié)泌包括實體認證 身份認證 協(xié)議 消息認證協(xié) 議 數(shù)據(jù)源認證協(xié)議和數(shù)據(jù)目的認證協(xié)議等 罔米防止假霉 篡改 否認等 攻擊 3 認證密鑰交換協(xié)議 這類協(xié)議將認證協(xié)議和密鑰交換協(xié)瀲結合在一 起 先對通信實體的身份進行認證 在認證成功的基礎上 為下一步安全通 信分酉己所使用的會話密镅 它是網(wǎng)絡通信中應用最普遍的一種安全擠議 翥 見的認證密鑰交換協(xié)議有互聯(lián)網(wǎng)密鑰交換 I K E 協(xié)議 分布式認證安全服 務 D A S S 協(xié)議 K e r b 目o s 認證協(xié)議 2 0 x 5 0 9 協(xié)議 等 4 電子商務協(xié)議 與上述擠議最為不弼的是 電子商務協(xié)議中主體往 往代表交易的雙方 其平玎益目標是不一致的 或者根本就是矛盾的 因此 電子商務協(xié)議最為關注的就是公平性 即協(xié)議應保證交易雙方都不能通過損 害對方利益而得到它不應得的利益 常見的電子商務協(xié)議有S E T 協(xié)議 I K P 游議等 c l a r k 和J a c o b 在文獻 2 2 中按安全協(xié)議所用的密碼算法對其進行了分類 列舉了一系列有研究意義和實用價值的安全協(xié)議 他們將現(xiàn)有的安全晦議進 行了如下的分類 1 無可信第三方的對稱密鑰協(xié)議 屬于這一類的典型協(xié)議包括以下的 I S O 系列協(xié)議f 2 3 I S O 對稱密鑰o n p 拈s 和t w o p a s s 單方認證協(xié)議 I s O 對稱 密鑰t w o a s s 雙方認證協(xié)議 I s O 對稱密鑰t K e e 巾a s s 雙方認證擠波 還膏 A n d r e w 安會R P C 協(xié)議1 蚓等 2 應用密碼校驗函數(shù) C C F 的認證協(xié)議 屬于這一類的典型協(xié)議包 括以下1 s O 系列協(xié)議 2 5 l I S O 應用C C F 的o n p a s s 幫M o 巾a s s 革方認證協(xié)議 I s 0 應用C C F 的柳o p s 雙方認證協(xié)議 I s O 應用c c F 的t r e e 巾a s s 雙方認 證協(xié)議 西南交通夫學碩士研究生學位論文 第j 7 頁 3 具有可信第三方的對稱密鑰協(xié)議 屬于這一類的典型協(xié)議包括N S 私鋸協(xié)議 2 礬 O t w a y I R e e s 協(xié)議 2 Y a h o m 協(xié)議f 撲 大嘴青蛙協(xié)議 D e n n i n 要 s a c c 協(xié)議 w o o L a m 協(xié)議 塒 4 對稱密鑰重復認證協(xié)議 屬于這一類的典型協(xié)議有K e r b e r o s 協(xié)議版 本5 N e u m a l l s l u b b l e b i n e 協(xié)議 K a o c h o w 重復認證協(xié)議嗍警 5 無可信第三方的公開密鑰協(xié)議 屬予這一類的典型協(xié)議包括以下 I s O 系列協(xié)議 I s O 公開密镅o n 巾8 s s 和t w o 巾a s g 單方認證協(xié)議 I s o 公開 密鑰c w o p a s s 雙方認證協(xié)議 I s O 公開密鑰t h r e o p a s s 雙方認證協(xié)議 I s O 公 開密鑰t w o 巾a s s 并行雙方認證協(xié)議 還有D i 髓e 扭e l h n 協(xié)議l l 等 6 具舂可信第三方的公開密鍘捧議 耩予這一類的典型協(xié)議有K s 公 鑰協(xié)議f 2 6 T M N 密鑰分發(fā)協(xié)議c 3 5 1 等 3 1 2 安壘協(xié)議系統(tǒng)模型 如果將協(xié)議及荬所處豹環(huán)境鞔為一個系統(tǒng) 那么在這個系統(tǒng)中 一般麗 言包括發(fā)送和接牧消息的誠實的主體和一個攻擊者 以及用于管理消息發(fā)送 相接收的規(guī)則 協(xié)議的臺法消息可被攻擊者藏敬 熏放和篡改 攻擊者將所 有已知的消息放入其知識集合K s K n o w l e d g es e l 中 誠實主體之闖交換 的任何消息都將被加入到攻擊者的K s 中 井屐 攻擊者可對K s 中的消息 進行操作 所得消息泡將加入到其K s 中 攻擊者可進行的攮I 乍至少包括級 聯(lián) 分離 加密和解密 一個被動攻擊者可在