本書內容主要包括以下部分：安全協議形式化分析背景及研究現狀。介紹了安全協議及形式化方法基本概念，安全協議形式化分析研究發(fā)展歷史和國內外研究現狀。形式化方法基本理論。對模態(tài)邏輯、模型檢測，定理證明三類形式化方法進行了詳細闡述和對比分析，介紹了Murφ和Spin具有代表性的形式化分析工具。安全協議。介紹了安全協議的基本概念及分類，從安全協議受攻擊類型角度提出安全協議形式化分析的必要性。