基于計算模型生成密碼學(xué)安全的安全協(xié)議代碼.pdf

1、目前安全協(xié)議的安全性仍是學(xué)術(shù)界關(guān)注的重點，但是安全協(xié)議的安全性分析僅僅停留在對安全協(xié)議抽象分析和驗證方面，很難應(yīng)用于日常研究中，而且在安全協(xié)議的代碼實現(xiàn)中難免會出現(xiàn)一些人為漏洞，這可能會給安全協(xié)議引入更大的漏洞。安全協(xié)議代碼的一般安全性（如數(shù)組下標(biāo)越界、內(nèi)存泄露、類型安全等），國內(nèi)外學(xué)者已經(jīng)做了很多有效的工作，但是關(guān)于安全協(xié)議實現(xiàn)代碼的研究人們做的工作很少，故本文重點關(guān)注安全協(xié)議代碼的密碼學(xué)安全性。
　　安全協(xié)議的最主要的安全性分

2、析方法有兩種，一種是構(gòu)造攻擊下的安全性分析，另外一種是模型形式化分析。本文基于安全協(xié)議的模型形式化分析方法，由代碼級出發(fā)，進(jìn)而研究安全協(xié)議的安全性，也就是對安全協(xié)議代碼的安全性進(jìn)行研究，以得到具有更強實用性的安全協(xié)議代碼。針對這些問題，本文首先對概率標(biāo)號遷移系統(tǒng)進(jìn)行研究，探索提出安全協(xié)議代碼的密碼學(xué)安全性模型；其次探索應(yīng)用概率進(jìn)程演算：Blanchet演算建模安全協(xié)議抽象規(guī)范的方法，給出安全協(xié)議抽象規(guī)范建模的模版；以Blanchet演算

3、建立的安全協(xié)議抽象規(guī)范模型為基礎(chǔ)，研究代碼轉(zhuǎn)換的可行性，并建立與Java代碼之間的映射關(guān)系。
　　本文探索從安全協(xié)議抽象規(guī)范模型生成安全協(xié)議Java代碼SP[Java]的方法。從進(jìn)程、角色、目標(biāo)多方面來建立Blanchet演算語言的映射模型，介紹轉(zhuǎn)換軟件的詞法分析器、語法分析器、簡化器、模板器的工作原理來闡述軟件的開發(fā)過程。最后開發(fā)生成安全協(xié)議Java代碼的自動化轉(zhuǎn)換軟件工具CV2JAVA。本文最后基于計算方法的自動化證明工具Cr