基于計算模型自動化驗證安全協(xié)議Java代碼認證性.pdf

1、隨著信息時代的發(fā)展，人們越來越關注隱私數據的保護，信息安全問題變得越來越突出。安全協(xié)議作為網絡通信中保證數據安全傳輸的基石，其安全性與有效性成為大眾關注的熱點，也是安全協(xié)議研究者的研究重點。形式化方法是分析與驗證安全協(xié)議的重要技術，主要包括：形式化安全協(xié)議，建立安全協(xié)議抽象模型，應用自動化分析工具驗證協(xié)議的安全屬性。安全協(xié)議形式化分析取得了豐碩成果，已提出了多個安全模型及發(fā)布了多種自動化分析工具。
　　盡管安全協(xié)議的形式化分析技術

2、能夠證明安全協(xié)議的安全屬性，但分析主要是建立在協(xié)議的抽象模型上，實用性差。實踐表明，已被正確證明的安全協(xié)議在編碼實現時會引入新的安全問題，因此分析安全協(xié)議代碼的密碼學安全屬性不可避免。目前對安全協(xié)議代碼的研究較少，模型抽取和代碼生成是其中的主要技術。本文基于模型抽取技術，對安全協(xié)議的Java源碼進行分析，抽取出其安全模型，并形式化為Blanchet演算代碼。使用基于計算方法的自動化證明工具CryptoVerif證明該源碼的認證性。主要工

3、作如下：
　　(1)描述了安全協(xié)議的形式化技術和安全協(xié)議代碼形式化技術。重點介紹計算方法的相關理論和模型抽取技術。
　　(2)分析安全協(xié)議的Java實現和Java的語法規(guī)范，建立安全協(xié)議實現的Java語法子集SubJ。介紹了基于計算方法的形式化語言 Blanchet演算，定義 SubJ與Blanchet演算間的語法映射關系。
　　(3)基于模型抽取技術，開發(fā)模型抽取工具SubJ2CV。該工具主要對協(xié)議的ubJ代碼首先進