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

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

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