基于UC框架的安全協(xié)議形式化分析.pdf

1、安全協(xié)議的分析和驗(yàn)證是保證所設(shè)計(jì)的協(xié)議滿足其安全性質(zhì)的重要技術(shù)手段，而借助形式化的方法或工具分析安全協(xié)議是非常有效和有必要的。然而，形式化分析方法都將密碼學(xué)原語(yǔ)抽象成符號(hào)化的操作，缺乏對(duì)于這些抽象的正確性的證明。因此，這些形式化方法不能用來(lái)證明當(dāng)抽象的原語(yǔ)被實(shí)際簡(jiǎn)單協(xié)議或者密碼學(xué)體制替換時(shí)，協(xié)議仍然是安全的。 近年來(lái)，有學(xué)者提出將兩種方法結(jié)合起來(lái)的框架：在保持形式化方法相對(duì)簡(jiǎn)單的情況下，使之也滿足密碼學(xué)可靠性。其中，UCSA(U

2、niversally Composable Symbolic Analysis）分析框架將形式化模型與UC框架結(jié)合起來(lái)，給出了證明一類(lèi)協(xié)議密碼學(xué)可靠性的一般方法。UCSA框架將Dolev-Yao模型中密碼學(xué)抽象操作與UC框架中的理想功能進(jìn)行了結(jié)合，使得通過(guò)形式化分析方法可以證明安全協(xié)議的在密碼學(xué)環(huán)境下的一些性質(zhì)。然而，UCSA框架在能夠分析協(xié)議類(lèi)型上有一定限制，只能分析一類(lèi)順序執(zhí)行的有限狀態(tài)協(xié)議，并且在協(xié)議中只能使用由不需要通信的本地算

3、法所表示的密碼學(xué)操作，如標(biāo)準(zhǔn)的公鑰加密操作，或者標(biāo)準(zhǔn)簽名操作。本文主要的工作是對(duì)UCSA框架進(jìn)行擴(kuò)展，主要成果和創(chuàng)新如下： 1.對(duì)UCSA中的形式化分析框架進(jìn)行了擴(kuò)展，定義了基于PAPi演算的形式化分析框架。一方面，以進(jìn)程演算為描述語(yǔ)言的協(xié)議能夠直觀的體現(xiàn)協(xié)議交互的特點(diǎn)；另一方面，PAPi演算中概率選擇操作算子為形式化模型中的協(xié)議加入了在行為層進(jìn)行概率選擇的能力，擴(kuò)展了形式化模型中能夠描述和分析的協(xié)議類(lèi)型； 2.對(duì)網(wǎng)絡(luò)通

4、信假設(shè)進(jìn)行了擴(kuò)展。在擴(kuò)展后的模型中支持?jǐn)呈挚刂仆ㄐ?、認(rèn)證通信、匿名通信(發(fā)送者匿名）等不同通信假設(shè)。而不同的假設(shè)是通過(guò)不同的輔助理想進(jìn)程所描述，可以根據(jù)所分析的協(xié)議選擇不同的通信模型； 3.對(duì)密碼學(xué)原語(yǔ)的抽象進(jìn)行了擴(kuò)展，加入了基于兩方協(xié)議的密碼學(xué)原語(yǔ)的抽象，如盲簽協(xié)議，承諾協(xié)議等。描述理想?yún)f(xié)議抽象的輔助進(jìn)程對(duì)應(yīng)于UC框架下相應(yīng)的理想功能，這使得形式化分析框架能夠保持其UC框架可靠的性質(zhì)； 4.擴(kuò)展了UC框架對(duì)應(yīng)與形式化框