基于增量式可滿足性求解的安全協(xié)議形式化驗(yàn)證方法.pdf

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

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