基于進(jìn)程演算的安全協(xié)議形式化研究.pdf

1、≥濤炙龜走冬SHANGHAIJIAOTONGUNIVERSITY博士學(xué)位論文DOCTORALDISSERTA耵ON論叉題目基王進(jìn)捏渲簋的塞壘墊邀型塞些垡窒學(xué)科專業(yè)鹽顯墊塾j魚里魚作者姓名題查巫目導(dǎo)教師——傅直墼塹撞答辯日期——————可以精確刻畫安全協(xié)議，在統(tǒng)一的框架下形式化描述和驗(yàn)證各種安全性質(zhì)GSPM中的進(jìn)程演算部分描述了協(xié)議參與主體的演化行為，邏輯部分使用了一系列推理規(guī)則推理主體的知識(shí)嵌入的知識(shí)推理系統(tǒng)具有可擴(kuò)展性，可以加入新的推

2、理規(guī)則更深入地分析安全協(xié)議此外。GSPM不為攻擊者行為單獨(dú)建模，既最大化了攻擊者能力。又簡(jiǎn)化了協(xié)議的分析過程3以GSPM為基礎(chǔ)分析驗(yàn)證安全性質(zhì)(a)基于GSPM，定義了一步可達(dá)關(guān)系和多步可達(dá)關(guān)系兩個(gè)概念，利用可達(dá)關(guān)系概念形式化地描述了安全協(xié)議的保密性，并以TMN協(xié)議為例作了實(shí)例研究(b)在給出了GSPM的LTS操作語義的基礎(chǔ)上，形式化地定義了安全協(xié)議的認(rèn)證性。并以NSPK協(xié)議為倒作了實(shí)例研究(c)基于GSPM的變體GSPM’，采用博弈思

3、想形式化地定義了公平交換協(xié)議的非否認(rèn)性和公平性，并以一種認(rèn)證郵件機(jī)制一MD機(jī)制為例作了實(shí)例研究(d)對(duì)其它安全性質(zhì)的形式化描述進(jìn)行了討論4在GSPM的變體GSPM的基礎(chǔ)上提出了一個(gè)環(huán)境敏感的抽象互模擬等價(jià)關(guān)系，形式化地定義了保密性和認(rèn)證性，并做了簡(jiǎn)單的實(shí)例分析5引入了符號(hào)化技術(shù)解決GSPM中等待輸入消息時(shí)導(dǎo)致的無限分叉問題在等待輸入一個(gè)匹配項(xiàng)時(shí)，將環(huán)境能產(chǎn)生的消息項(xiàng)分成有限類，產(chǎn)生有限個(gè)替換，選擇某個(gè)替換進(jìn)行遷移，并把替換記錄在遷移過程