理性安全協(xié)議形式化分析與驗(yàn)證研究.pdf

1、隨著電子商務(wù)的發(fā)展，考慮參與者的自利性，理性安全協(xié)議的設(shè)計(jì)和研究備受關(guān)注，公平性和安全性是理性安全協(xié)議尤為重要的性質(zhì)。雖然交替時(shí)序邏輯和交替時(shí)序認(rèn)知邏輯可對傳統(tǒng)安全協(xié)議的公平性和安全性等性質(zhì)進(jìn)行形式化分析與驗(yàn)證，但不適合于理性安全協(xié)議的形式化分析與驗(yàn)證。因此，以博弈邏輯為基礎(chǔ)，提出理性交替時(shí)序認(rèn)知邏輯，并用于對理性安全協(xié)議進(jìn)行形式化分析，為設(shè)計(jì)高效、公平和安全的理性安全協(xié)議提供保障，以及使用機(jī)器對理性安全協(xié)議的形式化分析與驗(yàn)證研究提供理

2、論基礎(chǔ)。所以對理性安全協(xié)議的形式化分析與驗(yàn)證研究具有重要的意義。本論文主要研究工作如下：
　　（1）基于博弈邏輯，在并行認(rèn)知博弈結(jié)構(gòu)中引入效用函數(shù)和偏好關(guān)系知識，得到理性并行認(rèn)知博弈結(jié)構(gòu)，并在合作模態(tài)算子中加入行為參數(shù)，提出理性交替時(shí)序認(rèn)知邏輯。
　　（2）基于理性交替時(shí)序認(rèn)知邏輯，建立理性參與者和理性安全協(xié)議形式化描述模型，并給出理性公平性、理性安全性的形式化描述，然后在理性并行認(rèn)知博弈結(jié)構(gòu)與擴(kuò)展式博弈的等價(jià)關(guān)系下，對具體

3、的理性交換協(xié)議進(jìn)行形式化分析。
　?。?）基于不動(dòng)點(diǎn)，對理性交替時(shí)序認(rèn)知邏輯的時(shí)序算子進(jìn)行描述，并給出理性交替時(shí)序認(rèn)知邏輯的推理系統(tǒng)?；诶硇詤⑴c者、理性公平性和理性安全性的形式化描述，運(yùn)用理性交替時(shí)序認(rèn)知邏輯的推理系統(tǒng)對具體的理性支付協(xié)議進(jìn)行形式化分析。
　?。?）基于交替時(shí)序邏輯的符號模型檢測算法，給出理性交替時(shí)序認(rèn)知邏輯的符號模型檢測算法，然后在此基礎(chǔ)上，給出理性安全協(xié)議的理性公平性和理性安全性符號模型檢測算法，并進(jìn)行