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

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

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

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