安全協(xié)議形式化模型串空間的研究.pdf

1、本文針對(duì)串空間模型的一些計(jì)算性質(zhì)作了詳細(xì)的分析，證明了串空間模型中保密性問(wèn)題的不可判定性，以及認(rèn)證問(wèn)題的不可判定性。關(guān)于保密性問(wèn)題的不可判定性，有一些研究者在其他一些模型之下給出過(guò)證明。盡管串空間模型和其他這些模型有許多不同之處，但是他們?cè)谥庇^背景上仍舊是相似的，所以本文借鑒了這些結(jié)果，在串空間模型中，通過(guò)一個(gè)從Post字對(duì)應(yīng)問(wèn)題的歸約，證明了保密性問(wèn)題的不可判定性。相比之下，現(xiàn)有針對(duì)認(rèn)證問(wèn)題的討論就要少很多。雖然保密性問(wèn)題和認(rèn)證問(wèn)題

2、在定義上相差甚遠(yuǎn)，但仍舊能通過(guò)一個(gè)從Post字對(duì)應(yīng)問(wèn)題的歸約，來(lái)證明認(rèn)證問(wèn)題的不可判定性。這也從一個(gè)側(cè)面驗(yàn)證了：保密性和認(rèn)證性在很多協(xié)議中是相互關(guān)聯(lián)的。另外，本文還就一種保密性不可判定性的證明進(jìn)行了討論，指出了其中的問(wèn)題，并提出了一種簡(jiǎn)單而有效的修正方法。盡管該證明是在另一個(gè)安全協(xié)議的形式化模型下作出的，但是由于所使用的歸約方法和被歸約的對(duì)象和我們的工作比較相似，對(duì)串空間中的形式化模型的研究也有相當(dāng)?shù)慕梃b意義。本文考察了串空間模型與