多方安全協(xié)議的形式化分析方法研究與應(yīng)用.pdf

1、本文首先對多方安全協(xié)議涉及的相關(guān)技術(shù)進(jìn)行研究，并給出一些典型的多方安全協(xié)議實(shí)例。多方安全協(xié)議由于涉及多種密碼學(xué)與信息安全技術(shù)，在進(jìn)行多方安全協(xié)議設(shè)計(jì)時(shí)不可避免地會(huì)出現(xiàn)一些缺陷。目前已經(jīng)有很多種研究安全協(xié)議的理論和方法，其中形式化方法是多方安全協(xié)議分析的主要方式。安全協(xié)議形式化分析方法主要分為三類：基于知識和信念的形式邏輯方法、模型檢測方法和定理證明方法。本文主要對基于邏輯的形式化方法與模型檢測技術(shù)及其在多方安全協(xié)議形式化分析中的應(yīng)用進(jìn)行

2、了系統(tǒng)研究，重點(diǎn)對SVO邏輯的擴(kuò)展及其在多方安全協(xié)議分析中的應(yīng)用進(jìn)行了研究。另外，我們還對基于博弈的ATL邏輯及其在多方安全協(xié)議的形式化分析中的應(yīng)用進(jìn)行了研究?？偟膩碚f，我們從理論和應(yīng)用兩個(gè)方面研究了多方安全協(xié)議的形式化分析相關(guān)技術(shù)。主要工作有以下幾個(gè)方面： 1.對多方安全協(xié)議涉及的組加密、可驗(yàn)證秘密分享方案、簽密技術(shù)進(jìn)行了研究，這些技術(shù)在多方安全協(xié)議的設(shè)計(jì)和改進(jìn)中非常重要。在此基礎(chǔ)上對門限簽密技術(shù)進(jìn)行研究，提出了一個(gè)基于橢圓曲線密碼體

3、制的(t，n)門限共享解簽密方案。該方案除了計(jì)算量與通信量少外，還具有保密性、認(rèn)證性、不可偽造性、不可否認(rèn)性、抵抗接收組成員欺騙等特點(diǎn)，可以滿足群體通信的要求。 2.對基于邏輯的安全協(xié)議形式化分析方法進(jìn)行研究，重點(diǎn)對SVO邏輯的基本符號、推理規(guī)則、推理過程、SVO邏輯的語義及SVO邏輯的特點(diǎn)進(jìn)行闡述，指出用SVO邏輯進(jìn)行安全協(xié)議(包括兩方和多方安全協(xié)議)形式化分析時(shí)存在一些亟待改進(jìn)的缺陷。 3.為了使SVO邏輯能用于分析兩方或多方安全協(xié)

4、議的不可否認(rèn)性、時(shí)限性、公平性及哈希函數(shù)的描述，我們對SVO邏輯形式化方法的各種擴(kuò)展方法進(jìn)行了系統(tǒng)地研究。并用擴(kuò)展SVO邏輯的推理規(guī)則對新ZG不可否認(rèn)協(xié)議進(jìn)行了形式化分析。 4.對一種基于SVO邏輯的新形式化方法進(jìn)行分析研究，用標(biāo)準(zhǔn)的SVO邏輯基本符號對其推理規(guī)則進(jìn)行重新描述，對其中出現(xiàn)的錯(cuò)誤進(jìn)行了改正，使其能夠更好地用于兩方或多方安全協(xié)議的形式化分析。另外，我們提出了一種新的SVO邏輯擴(kuò)展方法，并用它對改進(jìn)的電子支付協(xié)議進(jìn)行了形式化分

5、析。 5.SVO邏輯及其擴(kuò)展公理不僅可以用于簡單的安全協(xié)議安全性分析，也可以用于復(fù)雜的多方安全協(xié)議的不可否認(rèn)性、公平性、時(shí)限性、基于哈希函數(shù)的身份認(rèn)證等安全屬性的有效分析。我們對此進(jìn)行了研究，并利用SVO邏輯的公理和推理規(guī)則分別對一個(gè)不含TTP的多方不可否認(rèn)協(xié)議的不可否認(rèn)性和一個(gè)基于雙重組加密的多方不可否認(rèn)協(xié)議的公平性進(jìn)行了形式化證明。 6.對基于博弈的ATL邏輯及其在多方安全協(xié)議的形式化分析中的應(yīng)用進(jìn)行了研究。使用ATL邏輯和模型檢測