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

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