基于符號(hào)化模型檢測(cè)的安全協(xié)議驗(yàn)證.pdf

1、目前，安全協(xié)議的驗(yàn)證工作主要采用各種形式化方法，如邏輯證明和模型檢測(cè)?；谶壿嬜C明的安全協(xié)議分析在發(fā)現(xiàn)協(xié)議是不安全的之后不能給出現(xiàn)實(shí)的攻擊路徑，且協(xié)議的理想化過程及主觀性假設(shè)往往會(huì)影響分析的結(jié)果?；谀Ｐ蜋z測(cè)的安全協(xié)議分析雖然在近些年才開始受到人們的關(guān)注，但是其發(fā)展非常迅猛。特別是有序二叉決策樹(OBDD)等符號(hào)化技術(shù)的引入有效地解決了模型檢測(cè)面臨的狀態(tài)爆炸問題，產(chǎn)生了符號(hào)化模型檢測(cè)技術(shù)?，F(xiàn)在，符號(hào)化模型檢測(cè)技術(shù)已經(jīng)開始廣泛地應(yīng)用的安全

2、協(xié)議的驗(yàn)證工作中，各種符號(hào)化模型檢測(cè)工具，如SMV等應(yīng)運(yùn)而生。 IBS (Internet Business Server) 協(xié)議是卡內(nèi)基-梅隆大學(xué)開發(fā)的電子商務(wù)協(xié)議。到目前為止，還沒有文獻(xiàn)對(duì)IBS協(xié)議進(jìn)行基于符號(hào)化模型檢測(cè)的安全分析。為此，本文首先采用 SMV 符號(hào)化模型檢測(cè)工具對(duì)比較簡單的智力撲克協(xié)議(mental poker)的公平性進(jìn)行了安全驗(yàn)證。接著對(duì)IBS協(xié)議的不可否認(rèn)性、公平性等安全性能進(jìn)行了驗(yàn)證。結(jié)果表明IBS協(xié)