基于符號模型自動化生成安全協(xié)議代碼研究.pdf

1、在信息化高速發(fā)展的今天，人們越來越多的使用網(wǎng)絡(luò)來獲知信息，也越來越多的將個(gè)人信息提交到網(wǎng)絡(luò)，社交聊天工具和一些網(wǎng)絡(luò)應(yīng)用的普及使得人們越來越多的關(guān)注信息安全。安全協(xié)議是信息安全的重要組成部分，由兩個(gè)及以上的參與方在進(jìn)行一系列消息交換后達(dá)到某種既定目的。目前對安全協(xié)議進(jìn)行形式化分析，即用形式化建模方法分析驗(yàn)證安全協(xié)議的安全性，包括保密性和認(rèn)證性等，人們做了大量工作。但是僅僅分析安全協(xié)議抽象規(guī)范的安全是不夠的，因?yàn)樵诎踩珔f(xié)議具體實(shí)施的過程中可

2、能產(chǎn)生新的安全問題，因此安全協(xié)議實(shí)施安全成為安全協(xié)議研究的重要組成部分。
　　本文對安全協(xié)議實(shí)施安全進(jìn)行研究，完成以下工作：
　　（1）根據(jù)應(yīng)用PI演算與Java語言的操作語義關(guān)系，給出從應(yīng)用PI演算到Java語言的語法結(jié)構(gòu)的映射關(guān)系；
　?。?）提出從安全協(xié)議應(yīng)用PI演算實(shí)施生成安全協(xié)議 Java實(shí)施的方法。首先對應(yīng)用PI演算進(jìn)行詞法分析和語法分析，生成其語法樹；接著根據(jù)轉(zhuǎn)換映射，完成應(yīng)用PI演算語法樹到Java語法

3、樹的轉(zhuǎn)換，最終將具有安全性的應(yīng)用PI演算轉(zhuǎn)成Java實(shí)施；
　?。?）開發(fā)轉(zhuǎn)換工具PV2JAVA，可將安全協(xié)議應(yīng)用PI演算實(shí)施轉(zhuǎn)為安全協(xié)議Java實(shí)施；
　?。?）使用應(yīng)用PI演算對SAML2.0、Oauth2.0、改進(jìn)的Oauth2.0、SSHV2、TLS1.2五個(gè)安全協(xié)議進(jìn)行形式化建模分析，應(yīng)用ProVerif工具分析這些安全協(xié)議認(rèn)證性，然后使用PV2JAVA對這些安全協(xié)議的應(yīng)用PI演算實(shí)施轉(zhuǎn)為Java實(shí)施，調(diào)整后放入e