優化的匿名電子現金支付協議及其形式化驗證

摘要：針對匿名電子現金支付協議存在的缺陷，提出了一種能夠滿足多種安全屬性的優化協議。將會話密鑰的協商與使用分為兩個階段進行，確保協議密鑰保密性的實現；引入電子證書證明交易主體的身份，確保協議非否認性的實現；借助可信方傳遞付款收據，避免交易主體不誠實所導致的公平性缺失；引入FIP傳輸方式傳送電子貨幣和付款收據，確保實現可追究性與公平性，進一步增強協議的魯棒性。對優化協議進行形式化驗證，結果表明，優化協議滿足密鑰保密性、非否認性、公平性、可追究性、原子性等安全屬性。

關鍵詞：安全屬性；形式化驗證；密鑰保密性；非否認性；公平性；原子性

中圖分類號：TP393 文獻標志碼：A 文章編號：1001－3695(2010)08－3053－05