形式化驗(yàn)證安全協(xié)議Java代碼的安全性.pdf

1、安全協(xié)議分析和驗(yàn)證在信息安全領(lǐng)域占有重要地位。目前,安全協(xié)議形式化方法分析和驗(yàn)證主要集中在對(duì)實(shí)用性較差的安全協(xié)議抽象規(guī)范分析和驗(yàn)證方面,對(duì)注重實(shí)用性的安全協(xié)議代碼分析和驗(yàn)證涉及比較少;而靜態(tài)程序驗(yàn)證技術(shù)的應(yīng)用主要集中在程序正確性等方面,很少涉及代碼的密碼學(xué)安全性。因此本文將結(jié)合安全協(xié)議形式化分析與驗(yàn)證和靜態(tài)程序驗(yàn)證技術(shù)來(lái)分析和驗(yàn)證安全協(xié)議Java代碼密碼學(xué)安全性。本研究成果具有較強(qiáng)的理論意義和一定的應(yīng)用價(jià)值。
　　本文主要工作如下

2、:
　　1.對(duì)安全協(xié)議分析和驗(yàn)證做了一個(gè)完整的概述,說(shuō)明了進(jìn)行形式化分析的必要性,介紹了形式化分析的模型并詳細(xì)描述了形式化分析和驗(yàn)證的方法。
　　2.探討了 Java語(yǔ)言的形式化描述,具體介紹了 Java語(yǔ)句和表達(dá)式到應(yīng)用 PI演算語(yǔ)句的映射。同時(shí),介紹了程序靜態(tài)分析方法,研究了如何利用抽象語(yǔ)法樹對(duì)程序進(jìn)行預(yù)處理。
　　3.首先探索Java代碼抽象模型抽取方法和從Java代碼到應(yīng)用PI演算的映射;然后應(yīng)用一階定理證明器