網絡安全協議的形式化分析與驗證

所属分类:計算機安全  
出版时间:1970-1   出版时间:李建華、張愛新、薛質、 等 機械工業出版社 (2010-04出版)   作者:李建華 等 著   页数:214  

前言

隨著以Internet為代表的信息化浪潮席卷全球,信息技術的應用日益普及和廣泛,但Internet所具有的開放性、國際性和自由性在增加應用自由度的同時,對安全也提出了更高的要求,信息安全已成為關系到國家安全和經濟發展的重大戰略問題。安全協議(也稱密碼協議)是一個分布式算法,它規定了兩個或多個通信主體在一次通信過程中必須執行的一系列步驟。安全協議利用密碼技術實現開放網絡環境下的安全通信,達到信息安全的目的,廣泛地應用于身份認證、接入控制、密鑰分配、電子商務等領域。因此,安全協議作為實現信息安全的基礎,其自身的安全性間.題已成為安全研究的重要內容。由于網絡安全協議的重要性,從1978年第一個安全協議(Needham-Schroeder協議)誕生以來,人們對它的分析和設計就一直沒有停止過,也做出了卓有成效的工作。.最初,人們基于經驗和單純的軟件測試,采用攻擊檢驗方法來分析其安全性。由于安全協議往往運行在復雜的、不安全的網絡環境中,同時,新的攻擊方法層出不窮,產生的錯誤很難完全由人工識別。因此,很難保證對協議安全性分析的準確性。人們一致認為,必須采用形式化的方法和工具來分析密碼協議的安全性,即采用數學或邏輯模型,通過有效的程序來分析系統及其條件,以此確定一種在系統滿足條件情況下所得的證明是否正確的數學理論和方法。形式化方法在網絡安全協議分析中的作用主要體現在︰ヾ能使分析概念清晰;ゝ能發現協議設計中的錯誤;ゞ能證明協議的正確性;々能作為安全協議自動化分析、設計技術的理論指導。最先提出采用形式化方法分析密碼協議的是Needham和Schroeder。然而,在這一領域中第一項探索性的工作是由Dolev和Yao完成的,隨後由Dolev、Even和Karp在20世紀70年代後期和80年代初開發了一系列多項式時間算法來確定密碼協議的安全性。自1983年Dolev.Yao形式化模型提出以後,密碼協議形式化方法的研究有了長足的發展,到目前為止已形成了兩大流派,並且出現了理論融合的趨勢。一種流派稱為計算流派,它基于一個詳細的計算模型,安全性推理通常是通過構造一個“歸約為矛盾”類型的證明得到的,這里的“矛盾”是指計算復雜性領域中一個困難問題的有效解。隨機預言機模型(ROM)、作為該流派的代表,對于分析密碼算法的安全性有著公認的、廣泛的應用。另一流派稱為邏輯符號流派,它基于簡單而有效的形式化語言方法,對公理的應用可以基于邏輯證明、定理證明或狀態搜索技術。本書著重討論邏輯符號流派的主要S-作。目前,形式化理論在安全協議驗證中的應用主要集中在形式化分析、形式化設計及自動化工具開發3個方面。同時,隨著密碼技術的不斷發展和安全應用需求的不斷擴大。安全協議的結構也越來越復雜化,這些都對現有的形式化協議分析技術提出了很大的挑戰。

内容概要

  《網絡安全協議的形式化分析與驗證》概述了形式化技術在網絡安全協議分析、驗證中的主要應用原理及現狀;在此基礎上詳細地敘述了網絡安全協議的形式化分析技術、形式化設計技術;最後重點介紹了目前的形式化分析技術對當前典型應用環境下復雜、實用網絡安全協議的分析成果,包括IPSec協議、SSL協議、電子商務協議、移動通信安全協議及群組通信安全協議等。  信息安全是關系到國家安全和經濟發展的重大戰略問題,至關重要。安全協議作為實現信息安全的基礎,其自身的安全性問題已成為安全研究的重要內容。目前,針對安全協議的安全性驗證已形成了許多不同的流派、理論和方法。《網絡安全協議的形式化分析與驗證》理論與應用並重,深入淺出地介紹了各類形式化分析技術的基本原理及其在大型復雜安全協議分析中的實際應用。  《網絡安全協議的形式化分析與驗證》可作為信息安全專業高年級本科生教材,也可作為高等學校電子信息類、計算機類等相關專業的參考書。

书籍目录

前言第1章 緒論1.1 安全協議概述1.1.1 安全協議的基本概念1.1.2 安全協議的缺陷分析1.1.3 安全協議的攻擊手段1.1.4 安全協議形式化方法的必要性1.2 形式化技術基礎1.2.1 模態邏輯技術1.2.2 模型檢測技術1.2.3 定理證明技術1.3 形式化方法在安全協議驗證中的應用1.3.1 安全協議形式化理論發展現狀1.3.2 安全協議形式化方法發展趨勢1.4 本章 小結1.5 習題第2章 基于模態邏輯技術的安全協議分析方法2.1 BAN邏輯2.1.1 基本術語2.1.2 推理規則2.1.3 應用實例2.2 類BAN邏輯2.2.1 GNY邏輯2.2.2 AT邏輯2.2.3 SVO邏輯2.2.4 Kailar邏輯2.3 Bieber邏輯2.3.1 歷史模型2.3.2 KT5邏輯2.3.3 CKT5通信邏輯2.3.4 消息的解釋2.3.5 認證與保密2.4 非單調邏輯2.4.1 安全協議的Nonmonotomic邏輯描述2.4.2 安全協議的Nonmonotomic邏輯分析2.5 本章 小結2.6 習題第3章 基于模型檢測技術的安全協議分析方法3.1 Dolev Yao模型3.2 通信進程方法3.2.1 CSP的基本概念3.2.2 CSP的網絡模型3.2.3 協議安全性質的CSP描述3.2.4 CSP協議分析3.3 NRL協議分析器3.3.1 協議描述3.3.2 協議分析3.3.3 實例3.4 模型檢測工具Mur3.4.1 Mur系統3.4.2 Mur協議分析過程3.4.3 Mur協議分析實例3.5 模型檢測工具ASTRAL3.6 協議分析工具BRUTUS3.6.1 BRUTUS協議描述模型3.6.2 BRUTUS協議屬性邏輯3.6.3 BRUTUS協議驗證算法3.6.4.BRUTUS協議分析實例3.7 本章 小結3.8 習題第4章 基于定理證明的安全協議分析方法4.1 Paulson歸納法4.1.1 Paulson歸納法簡介4.1.2 Paulson歸納法的自動化理論4.1.3 Paulson歸納法協議分析示例4.2 Schneider階函數4.2.1 階函數的定義4.2.2 階函數定理4.2.3 協議分析實例4.2.4 基于階函數的自動化驗證技術4.3 串空間4.3.1 基本概念4.3.2 協議入侵者描述4.3.3 安全屬性的表示4.3.4 協議分析舉例4.3.5 認證測試方法4.4 重寫逼近法4.4.1 預備知識4.4.2 逼近技術4.4.3 對NS公鑰協議的描述與分析4.5 不變式產生技術4.5.1 基本概念4.5.2 描述攻擊者不可知項集合的不變式4.5.3 描述攻擊者可知項集合的不變式4.6 本章 小結4.7 習題第5章 安全協議的形式化設計方法5.1 合成協議模型及其安全性5.1.1 HT模型5.1.2 協議的組合5.2 Fail-Stop協議5.2.1 Fail-Stop協議及其分析5.2.2 復雜協議5.3 BSW簡單邏輯5.3.1 模型5.3.2 邏輯5.4 本章 小結5.5 習題第6章 Internet密鑰交換協議及其分析6.1 Internet密鑰交換協議概述6.1.1 階段1主模式交換6.1.2 階段1野蠻模式交換6.1.3 階段2快速模式交換6.2 IKE三協議的形式化分析6.2.1 采用NRL協議分析器進行形式化分析6.2.2 利用擴展BSW邏輯分析6.3 IKEV2協議概述6.3.1 IKEV2密鑰交換6.3.2 密鑰算法協商6.3.3 加密密鑰與認證密鑰6.4 IKEV2協議的形式化分析6.4.1 擴展串空間理論6.4.2 IKEV2協議分析6.5 本章 小結6.6 習題第7章 電子商務安全協議及其分析7.1 早期的電子商務安全協議7.1.1 Digicash協議7.1.2 First Virtual協議7.1.3 Netbill協議7.2 SSL協議及其分析7.2.1 SSL協議介紹7.2.2 SSL協議的形式化分析7.3 SET協議及其分析7.3.1 SET協議的流程7.3.2 雙重簽名技術7.3.3 數字信封v7.3.4 SEL協議的形式化分析7.4 本章 小結7.5 習題第8章 移動通信安全協議及其分析8.1 移動通信安全協議8.1.1 第1代移動通信安全協議8.1.2 第2代移動通信安全協議8.1.3 第3代移動通信安全協議8.2 AUTLOG認證邏輯對AKA協議的分析8.2.1 AUTLOG認證邏輯8.2.2 協議的形式化描述8.2.3 假設前提8.2.4 協議目標8.2.5 形式化證明8.3 利用認證測試方法對3GPP-AKA,協議進行安全性分析8.3.1 移動用戶與移動核心網之間的安全性驗證8.3.2 服務網絡基站與移動核心網之間的安全性驗證8.3.3 服務網絡基站與移動用戶之間的安全性驗證8.4 本章 小結8.5 習題第9章 群組通信安全協議及其分析9.1 群組通信概述9.2 群組密鑰管理協議9.3 密鑰管理方案9.3.1 集中式密鑰管理方案9.3.2 分布式密鑰分發方案9.3.3 分擔式密鑰協商方案9.4 群組密鑰交換協議的形式化描述及安全性分析9.4.1 AT-GDH協議9.4.2 AT-GDH2協議9.4.3 AT-GDH3協議9.5 本章 小結9.6 習題參考文獻出版說明

章节摘录

插圖︰6.密碼系統缺陷密碼系統缺陷是指協議中使用的密碼算法不合適或對密碼算法的實現不當,而導致協議不能完全滿足所要求安全需求而產生的缺陷。應該指出的是,隨著攻擊手段與技術的不斷翻新,以上缺陷並不能涵蓋網絡安全協議在實際應用中的所有可能出現的漏洞。一個安全協議在運行過程中,假如有攻擊者存在,並且沒有被系統或者誠實角色所察覺,同時攻擊者在參與協議運行過程中並沒有利用任何密碼學上的漏洞,那麼我們就說該協議存在設計上的漏洞。本書只討論由于協議設計漏洞所產生的協議缺陷。1.1.3 安全協議的攻擊手段針對信息系統的攻擊主要有兩種形式,即被動竊听和主動分析。前者是通過非法搭線竊听,截取通信信息後進行分析以獲得機密內容或敏感信息︰後者指對通信信息進行非法修改,包括插入非法信息、重放陳舊信息、刪除通信消息和修改通信消息等。一個被動攻擊者可以在線竊听敏感信息,而一個主動攻擊者則可截獲數據包並對其進行任意的修改,甚至可以偽裝成通信主體,欺騙誠實主體與其進行非法的通信。實現這些攻擊的方法很多,比如可以對系統采用的密碼系統進行數學分析、旁路攻擊以破解機密信息並對系統進行即時監听等;另外,還有一類很重要的攻擊方式,那就是利用協議本身的漏洞攻擊信息系統,采用這種攻擊方式不需要很大的計算量,往往成為黑客的主要攻擊手段。下面簡要介紹一些由于協議設計漏洞而產生的針對安全協議的攻擊方式。1.中間人攻擊在中間人攻擊中,攻擊者將自己偽裝于兩個通信主體之間進行通信,甚至可以冒充任一主體的身份向對方發送消息。考慮以下協議︰在用戶Alice、Bob不知道對方私鑰的情況下,用戶Alice希望采用公鑰密碼技術向Bob發送一條秘密消息,協議使用︰RSA公鑰加密算法。

编辑推荐

《網絡安全協議的形式化分析與驗證》︰安全協議及其形式化技術的基本概念、原理和方法,安全協議的形式化分析方法,安全協議的形式化設計技術,形式化技術在復雜安全協議分析中的典型應用。

图书封面


    網絡安全協議的形式化分析與驗證下載



用户评论 (总计1条)

 
 

  •     導師說書要比論文落後5年,所以看不懂論文的時候再看書。我就看了一部分,覺得還可以,就是沒有網絡安全基礎的話,會很費勁
 

計算機與互聯網 PDF免费下载,計算機安全PDF免费下载。 计算机教程网 

计算机教程网 @ 2017