密碼協(xié)議本身的安全問題一直以來都倍受關(guān)注。邏輯分析能夠有效地發(fā)現(xiàn)密碼協(xié)議的潛在缺陷，避免使用不安全協(xié)議帶來的損失。具有知識非單調(diào)性的密碼協(xié)議的分析需要能夠表示非單調(diào)性的邏輯。我們將首先用“forget”擴展動態(tài)認知邏輯語言并給出其精確的語法和語義描述具有知識非單調(diào)性的密碼協(xié)議，其次用克里普克(Kripke)模型結(jié)合寄存器模型表示協(xié)議中各主體的知識以及協(xié)議運行過程中主體知識的變化，協(xié)議整個運行過程被完全地形式化。這個形式化過程就是對協(xié)議的分析過程，協(xié)議運行的最后一步形式化結(jié)果即為協(xié)議的分析結(jié)果，因此協(xié)議的安全性也在模型圖中自然呈現(xiàn)，并進一步表明我們的分析是有效的。