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

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

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

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