非否認(rèn)協(xié)議的UC可靠的形式化驗(yàn)證.pdf

1、在網(wǎng)絡(luò)時代，人們對安全協(xié)議的安全性要求越來越高，而借助形式化方法對安全協(xié)議進(jìn)行安全分析是檢驗(yàn)安全協(xié)議安全性的重要手段。但是形式化的驗(yàn)證方式是建立在密碼學(xué)完備的基礎(chǔ)上的，也就是說被形式化驗(yàn)證證明為安全的協(xié)議，在現(xiàn)實(shí)中不一定是安全的。所以，Canetti提出了相對于UC框架是可靠的UCSA框架，而后人們對UCSA框架做出了擴(kuò)展，把UCSA框架轉(zhuǎn)變?yōu)榛赑APi演算，并且加入了更多的通信信道假設(shè)和密碼學(xué)抽象。在本文中，我們一方面對前人的工作做

2、出了進(jìn)一步的擴(kuò)充和改進(jìn)，另外一方面我們也用UCSA框架對某一個具體的協(xié)議進(jìn)行了安全分析。本文的主要貢獻(xiàn)如下：首先，本文在前人的基礎(chǔ)上添加了可恢復(fù)的認(rèn)證通信這一種新的通信假設(shè)，使之可以分析更多種類的安全協(xié)議。為此，我們定義了可恢復(fù)的認(rèn)證通信的輔助進(jìn)程，定義了可恢復(fù)的認(rèn)證通信的理想功能并且證明了在擴(kuò)展后的UCSA框架下，形式化安全與UC安全的等價性。我們對UCSA框架下的簡單協(xié)議進(jìn)行了擴(kuò)充，使之能夠使用新加入的可恢復(fù)的認(rèn)證通信假設(shè)。我們還定

3、義了新的簡單協(xié)議翻譯規(guī)則和新的攻擊者策略和新的協(xié)議事件來反映所添加的可恢復(fù)的認(rèn)證通信假設(shè)。其次，我們在本文中用擴(kuò)展后的UCSA框架對Zhou-Gollmann協(xié)議（以下簡稱ZG協(xié)議）進(jìn)行了安全分析，分析它在無可恢復(fù)的認(rèn)證通信假設(shè)和在有可恢復(fù)的認(rèn)證通信假設(shè)的情況下是否符合非否認(rèn)性的形式化定義。本文用UCSA框架及其變體對某一個具體的安全協(xié)議做出從頭到尾的分析。本文根據(jù)ZG協(xié)議的定義對協(xié)議的參與者用簡單協(xié)議進(jìn)行建模，然后用簡單協(xié)議到形式化協(xié)