密碼協議安全性證明系統解析器的設計與實現
2010-12-31 00:00:00李安樂陳楠顧純祥祝躍飛
計算機應用研究 2010年9期
摘要：可證明安全性是密碼協議安全性評估的重要依據，但手寫安全性證明容易出錯且正確性難以判定，利用計算機輔助構造游戲序列進而實現自動化證明是當前一種可行的方法。為此提出一種基于進程演算的密碼協議形式化描述模型，定義了描述密碼協議安全性證明中攻擊游戲的語法規則，并借助工具LEX和YACC，設計出解析器程序，將密碼協議及其安全性的形式化描述解析為自動化安全性證明系統的初始數據結構，并用實例來說明這種方法的可行性。
關鍵詞：可證明安全；自動化；進程演算
中圖分類號：TP309 文獻標志碼：A 文章編號：1001－3695(2010)09－3529－04
