基于增量式可滿足性求解的安全協議形式化驗證方法.pdf

1、隨著現代計算機技術和網絡技術的不斷更新，它們的應用領域也在向著更寬更深的方向發(fā)展，這也對計算機網絡安全提出了更高的要求。被設計用來解決這一問題的安全協議在一定程度上為網絡通信的正常運行起到了積極的作用。但是，由于其自身設計中的一些缺陷而最終導致的安全漏洞也成為了現代非常嚴重的網絡安全問題。所以人們就在安全協議設計與分析中投入了大量的工作。 安全協議設計規(guī)則為安全協議的制定提供了標準，而安全協議分析為安全協議能夠成功實現其安全性能

2、提供了保障。并且，隨著現代通信技術的不斷發(fā)展和網絡技術的廣泛應用，這兩個方面越來越受到人們的關注。這其中就包括對安全協議的形式化分析這一重要內容。 安全協議的形式化分析大體來說有三種方法，形式邏輯，模型檢驗和定理證明。其中，作為形式化分析的重要組成部分和有效分析手段的模型檢驗技術在分析安全協議這一過程中更是凸顯了其重要的作用和地位。其中，有一種基于可滿足性問題的模型檢驗技術已經在安全協議形式化分析中得到了應用。 本文的主