密碼協(xié)議安全性證明系統(tǒng)解析器的設(shè)計(jì)與實(shí)現(xiàn)

摘要：可證明安全性是密碼協(xié)議安全性評(píng)估的重要依據(jù)，但手寫(xiě)安全性證明容易出錯(cuò)且正確性難以判定，利用計(jì)算機(jī)輔助構(gòu)造游戲序列進(jìn)而實(shí)現(xiàn)自動(dòng)化證明是當(dāng)前一種可行的方法。為此提出一種基于進(jìn)程演算的密碼協(xié)議形式化描述模型，定義了描述密碼協(xié)議安全性證明中攻擊游戲的語(yǔ)法規(guī)則，并借助工具LEX和YACC，設(shè)計(jì)出解析器程序，將密碼協(xié)議及其安全性的形式化描述解析為自動(dòng)化安全性證明系統(tǒng)的初始數(shù)據(jù)結(jié)構(gòu)，并用實(shí)例來(lái)說(shuō)明這種方法的可行性。

關(guān)鍵詞：可證明安全；自動(dòng)化；進(jìn)程演算

中圖分類(lèi)號(hào)：TP309 文獻(xiàn)標(biāo)志碼：A 文章編號(hào)：1001－3695(2010)09－3529－04