随着现代社会向信息化方向不断迈进,越来越多的传统的信息保存和传播媒介开始被数字化的媒介所取代。其中,企业内部交流信息和文件的渠道也开始由传统的纸质渠道逐渐转化为电子渠道。电子邮件、电子文档、电子聊天记录、电子文件摘要、电子档案整理等等,逐渐取代书面档案、书面记录和书面摘要,成为企业管理中档案管理方式的主流。电子文档以其节约成本、环保、高效等特点受到广大企事业单位的青睐。但是直到2004年8月,《中华人民共和国电子签名法》(下简称《电子签名法》)的出台,才对电子文档的法律效力作了规定。本文写作的目的是,描述一种本实验室与他人合作开发的,符合《电子签名法》要求的电子签名系统软件,并且利用形式化描述和自动化分析的方法,对该软件中使用的安全协议是否符合安全性要求进行分析和验证,证明该软件确实能够保证签名有效,从而,为该软件应用于实际生产和生活中打下坚实的基础,同时为该软件,以及其他同类的电子签名软件在安全性方面的改进和提高提供一定参考。本文的主要内容如下。首先,本文对安全协议的形式化分析方法做了一个简单的介绍,并且阐明了网络安全协议形式化建模工具GSPM的优点和本文使用GSPM作为形式化建模工具的原因;其次,本文描述了一个符合《电子签名法》中规定的具有法律效力的电子签名要求的电子签名系统软件,并且将该软件中使用的主要安全协议加以提取和分析。再次,本文对该软件中使用的安全协议使用GSPM进行形式化建模,并使用基于GSPM的安全协议形式化验证工具GSPMC对该电子签名系统中使用的安全协议进行验证。同时,对该电子签名系统中,除了安全协议以外的一些保证安全的措施加以介绍、分析和验证。最后,本文给出该电子签名系统的安全性是否符合要求的结论并将该电子签名系统的安全性进行一个广义上的拓展,讨论一些条件更宽泛的情况。本文的主要研究方法是形式化建模和基于形式化分析的自动验证的方法。并对电子签名系统中使用的安全协议进行形式化建模,提取电子签名系统中所使用的安全协议,使用GSPM将其进行形式化描述,使用基于GSPM的安全协议安全性验证自动化工具GSPMC对上述安全协议的安全性进行分析,进而对分析结果提出结论和解决方案。本文从保密性和认证性两种性质出发,验证了该电子签名系统使用的安全协议在局域网和广域网下,在GSPM模型的条件限定下没有保密性和认证性方面安全漏洞的;并对其他方面可能的安全隐患作了分析,并提出解决方案。同时为该电子签名系统进一步的改进和完善提供依据和建议,并且对其他同类电子签名系统的开发和将来的电子签名系统的发展有一定参考价值。