基于進程代數的CSP 方法是一種重要的形式化協議分析驗證方法。本文首先簡單介紹了CSP 相關理論，并以NSPK 協議為例系統概述了安全協議的CSP 建模方法。為更好的查明協議的安全缺陷，重點研究如何在CSP的體系結構中對協議的安全屬性進行形式化描述。并最終提出秘密性、認證性、不可否認性、匿名性的形式化提煉檢測目標，為進一步使用模型檢測器進行協議驗證奠定了理論和技術基礎。
關鍵詞建模 進程 入侵者 安全屬性
Abstract: It is an important formal method in protocol’s analysis that CSP approach based on the process algebra. In this paper, the CSP theory is introduced in brief and then the CSP modeling Approach of security protocols is summarized by using the NSPK example. It is studied formal description of Security Properties in the CSP system frame in order to find out the bug of security protocols in effect. In finally, it is presented the refine verifying targets of secrecy、authentication、non-repudiation and anonymity in formal which given the theoretical foundation for the model checking.
Keywords: Modeling, Process, Intruder, Security Property