幫助中心 | 我的帳號 | 關於我們
進階搜尋
car

同類熱銷排行榜

最近瀏覽的商品

網路安全協議的形式化分析/新一代信息技術網路空間安全系列叢書

  • 作者：編者:付玉龍//曹進//李暉//藺如嫣|責編:李惠萍
  • 出版社：西安電子科大
  • ISBN：9787560675176
  • 出版日期：2025/04/01
  • 裝幀：平裝
  • 頁數：240
人民幣：RMB 42 元      售價：元
放入購物車
加入收藏夾
內容大鋼
    本書系統地講解了利用形式化方法對網路協議及系統進行安全性分析的原理、流程和典型工具，結合科研實例深入淺出地介紹了形式化安全方法的範疇、類型和使用技巧。全書內容密切圍繞國家安全戰略需求，緊跟時代發展，是對多年來該領域的科學研究與工程實踐中基本原理與共性技術的歸納總結。本書分為三個單元，共8章。第一單元（第1?4章）主要介紹網路協議形式化安全分析方法的相關基礎知識，包括緒論、離散數學基礎知識、密碼學基礎知識、協議工程與軟體工程基礎知識等內容，明確了採用形式化方法對電腦系統中網路協議和軟體的安全性進行分析的主要步驟，以及形式化安全方法發展的歷史和趨勢。第二單元（第5?7章）主要介紹現有的網路協議形式化安全分析方法，系統地講解了相關方法在確保通信協議和軟體實現的安全性方面的關鍵應用，包括基於演繹推理和自動機模型的形式化安全方法和基於進程演算的形式化方法。第三單元（第8章）主要介紹通信軟體安全性的形式化驗證實例，展示了形式化方法在實際安全應用中的具體實施和效果。
    本書適合作為高等院校網路空間安全、信息安全專業或其他相關專業本科生和研究生的教材，也可供相關領域的科研人員參考。
作者介紹
編者:付玉龍//曹進//李暉//藺如嫣|責編:李惠萍
目錄
第一單元  基礎知識
第1章  緒論
  1.1  形式化安全方法概述
  1.2  通信安全中的形式化方法
  1.3  軟體安全中的形式化方法
    1.3.1  軟體安全的重要性與漏洞歷史案例
    1.3.2  軟體漏洞的挑戰與統計
    1.3.3  軟體安全技術與形式化方法的發展
  本章小結
  本章習題
第2章  離散數學基礎知識
  2.1  數理邏輯
    2.1.1  命題邏輯與安全斷言
    2.1.2  命題邏輯的推理理論
    2.1.3  一階邏輯
    2.1.4  時序邏輯與高階邏輯
  2.2  集合論
    2.2.1  集合代數
    2.2.2  二元關係與函數
  2.3  代數結構
    2.3.1  代數系統
    2.3.2  群、環與格
  2.4  圖論
    2.4.1  圖的基本概念
    2.4.2  樹
  本章小結
  本章習題
第3章  密碼學基礎知識
  3.1  密碼基本理論與技術概述
    3.1.1  密碼學相關術語的定義
    3.1.2  兩類加密演算法
  3.2  對稱密碼
    3.2.1  流密碼
    3.2.2  分組密碼
  3.3  公鑰密碼體制
    3.3.1  公鑰密碼體制的基本概念
    3.3.2  RSA密碼機制
    3.3.3  基於身份的密碼機制
    3.3.4  橢圓曲線密碼機制
    3.3.5  無證書密碼機制
  3.4  Hash函數
    3.4.1  Hash函數用來提供認證的基本使用方式
    3.4.2  Hash函數應滿足的條件
    3.4.3  第Ⅰ類生日攻擊
    3.4.4  第Ⅱ類生日攻擊
  3.5  數字簽名
    3.5.1  數字簽名演算法
    3.5.2  橢圓曲線數字簽名演算法
    3.5.3  代理簽名演算法
    3.5.4  聚合簽名演算法

    3.5.5  多重簽名演算法
  本章小結
  本章習題
第4章  協議工程與軟體工程基礎知識
  4.1  協議工程
    4.1.1  協議設計原理
    4.1.2  協議安全
    4.1.3  協議驗證技術
  4.2  軟體工程
    4.2.1  軟體生命周期
    4.2.2  軟體安全
    4.2.3  軟體驗證技術
  本章小結
  本章習題
第二單元  形式化安全分析方法
第5章  基於演繹推理的形式化安全方法
  5.1  BAN邏輯
    5.1.1  BAN邏輯的定義
    5.1.2  形式化描述
    5.1.3  形式化的協議驗證目標
  5.2  GNY邏輯
    5.2.1  基本術語
    5.2.2  推理規則
  5.3  SVO邏輯
    5.3.1  SVO邏輯的語法
    5.3.2  SVO邏輯推理公理
    5.3.3  SVO邏輯推理規則
  5.4  演繹推理實例分析
    5.4.1  使用BAN邏輯分析Kerberos協議
    5.4.2  使用改進GNY邏輯分析Kerberos*協議
    5.4.3  使用SVO邏輯分析改進Otway-Rees協議
  本章小結
  本章習題
第6章  基於自動機模型的形式化安全方法
  6.1  FSM模型
    6.1.1  圖靈機與系統狀態機
    6.1.2  有限自動機的定義及分類
    6.1.3  自動機模型的擴展
    6.1.4  自動機模型的應用
  6.2  Petri網模型
    6.2.1  Petri網的原理
    6.2.2  Petri網的擴展
    6.2.3  Petri網的應用
  6.3  標籤轉移系統（LTS）模型
    6.3.1  標籤轉移系統的基本概念
    6.3.2  標籤轉移系統的擴展
    6.3.3  標籤轉移系統的應用
  6.4  標準形式化語言
    6.4.1  SDL語言
    6.4.2  ESTELLE語言

  6.5  自動化驗證工具
    6.5.1  SPIN
    6.5.2  UPPAAL
  6.6  實例分析與實驗——用UPPAAL驗證Pr?t ? Voter電子投票協議
  本章小結
  本章習題
第7章  基於進程演算的形式化方法
  7.1  進程演算
    7.1.1  進程代數體系
    7.1.2  進程演算方法
  7.2  CSP與CCS
    7.2.1  CSP
    7.2.2  CCS
  7.3  標準語言——LOTOS
  7.4  擴展模型
    7.4.1  Security Pi Calculus
    7.4.2  Applied Pi Calculus
    7.4.3  Ambient Calculus
  7.5  自動化工具
    7.5.1  ProVerif
    7.5.2  Tamarin
  7.6  實例分析與實驗
    7.6.1  使用Tamarin驗證Diffie Hellman協議
    7.6.2  使用ProVerif分析5G-AKA協議
  本章小結
  本章習題
第三單元  形式化安全方法的綜合應用
第8章  通信軟體安全性的形式化驗證實例
  8.1  通信軟體的形式化安全驗證流程
    8.1.1  通信軟體設計的安全性驗證流程
    8.1.2  通信軟體代碼的安全性驗證流程
  8.2  通信軟體形式化安全驗證實例
    8.2.1  分析對象
    8.2.2  CHAP軟體設計安全性驗證
    8.2.3  CHAP軟體代碼一致性驗證
  本章小結
參考文獻

  • 商品搜索：
  • | 高級搜索
首頁│ 新手上路│ 客服中心│ 關於我們│ 聯絡我們│ Top↑│
Copyrightc 1999~2008 美商天龍國際圖書股份有限公司 臺灣分公司. All rights reserved.
營業地址:臺北市中正區重慶南路一段103號1F 105號1F-2F
讀者服務部電話：02-2381-2033 02-2381-1863　時間：週一-週五 10:00-17:00
　服務信箱：bookuu@69book.com 客戶、意見信箱:cs@69book.com
ICP證：浙B2-20060032