基于進(jìn)程代數(shù)的CSP 方法是一種重要的形式化協(xié)議分析驗(yàn)證方法。本文首先簡(jiǎn)單介紹了CSP 相關(guān)理論，并以NSPK 協(xié)議為例系統(tǒng)概述了安全協(xié)議的CSP 建模方法。為更好的查明協(xié)議的安全缺陷，重點(diǎn)研究如何在CSP的體系結(jié)構(gòu)中對(duì)協(xié)議的安全屬性進(jìn)行形式化描述。并最終提出秘密性、認(rèn)證性、不可否認(rèn)性、匿名性的形式化提煉檢測(cè)目標(biāo)，為進(jìn)一步使用模型檢測(cè)器進(jìn)行協(xié)議驗(yàn)證奠定了理論和技術(shù)基礎(chǔ)。
關(guān)鍵詞建模 進(jìn)程 入侵者 安全屬性
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