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