對(duì)電子簽名系統(tǒng)的形式化描述和安全性分析.pdf

1、隨著現(xiàn)代社會(huì)向信息化方向不斷邁進(jìn)，越來(lái)越多的傳統(tǒng)的信息保存和傳播媒介開(kāi)始被數(shù)字化的媒介所取代。其中，企業(yè)內(nèi)部交流信息和文件的渠道也開(kāi)始由傳統(tǒng)的紙質(zhì)渠道逐漸轉(zhuǎn)化為電子渠道。電子郵件、電子文檔、電子聊天記錄、電子文件摘要、電子檔案整理等等，逐漸取代書(shū)面檔案、書(shū)面記錄和書(shū)面摘要，成為企業(yè)管理中檔案管理方式的主流。電子文檔以其節(jié)約成本、環(huán)保、高效等特點(diǎn)受到廣大企事業(yè)單位的青睞。但是直到2004年8月，《中華人民共和國(guó)電子簽名法》（下簡(jiǎn)稱(chēng)《電子簽

2、名法》）的出臺(tái)，才對(duì)電子文檔的法律效力作了規(guī)定。 本文寫(xiě)作的目的是，描述一種本實(shí)驗(yàn)室與他人合作開(kāi)發(fā)的，符合《電子簽名法》要求的電子簽名系統(tǒng)軟件，并且利用形式化描述和自動(dòng)化分析的方法，對(duì)該軟件中使用的安全協(xié)議是否符合安全性要求進(jìn)行分析和驗(yàn)證，證明該軟件確實(shí)能夠保證簽名有效，從而，為該軟件應(yīng)用于實(shí)際生產(chǎn)和生活中打下堅(jiān)實(shí)的基礎(chǔ)，同時(shí)為該軟件，以及其他同類(lèi)的電子簽名軟件在安全性方面的改進(jìn)和提高提供一定參考。 本文的主要內(nèi)容如下。

3、 首先，本文對(duì)安全協(xié)議的形式化分析方法做了一個(gè)簡(jiǎn)單的介紹，并且闡明了網(wǎng)絡(luò)安全協(xié)議形式化建模工具GSPM的優(yōu)點(diǎn)和本文使用GSPM作為形式化建模工具的原因；其次，本文描述了一個(gè)符合《電子簽名法》中規(guī)定的具有法律效力的電子簽名要求的電子簽名系統(tǒng)軟件，并且將該軟件中使用的主要安全協(xié)議加以提取和分析。再次，本文對(duì)該軟件中使用的安全協(xié)議使用GSPM進(jìn)行形式化建模，并使用基于GSPM的安全協(xié)議形式化驗(yàn)證工具GSPMC對(duì)該電子簽名系統(tǒng)中使用的安

4、全協(xié)議進(jìn)行驗(yàn)證。同時(shí)，對(duì)該電子簽名系統(tǒng)中，除了安全協(xié)議以外的一些保證安全的措施加以介紹、分析和驗(yàn)證。最后，本文給出該電子簽名系統(tǒng)的安全性是否符合要求的結(jié)論并將該電子簽名系統(tǒng)的安全性進(jìn)行一個(gè)廣義上的拓展，討論一些條件更寬泛的情況。 本文的主要研究方法是形式化建模和基于形式化分析的自動(dòng)驗(yàn)證的方法。并對(duì)電子簽名系統(tǒng)中使用的安全協(xié)議進(jìn)行形式化建模，提取電子簽名系統(tǒng)中所使用的安全協(xié)議，使用GSPM將其進(jìn)行形式化描述，使用基于GSPM的安全