论文部分内容阅读
工业控制系统(Industrial Control Systems,ICS)是一个国家的经济命脉,普遍应用在国民经济的各个领域,是我们国家很多关键基础设施的重要组成部分,其安全性不言而喻。而随着“中国制造2025”的提出,工业控制系统和网络互连已经成为不可避免的趋势,目前由于我国在工业控制系统应用上缺乏核心技术,普遍采用国外的工业控制系统协议和工控设备,近几年在工业控制安全防御方面刚刚起步,目前对协议的安全分析迫在眉睫,而安全协议形式化分析是最方便有效的是基于模型的形式化分析方法。本文研究的TLS协议用于保障工业网络控制系统中EtherNet/IP协议数据传输的安全。1.首先由于EtherNet/IP协议存在安全隐患,以此协议为主的工业控制系统存在信息被窃取以及篡改的威胁。其保障信息传输安全性取决于传输层和应用层之间的TLS协议的安全保障能力,而目前EtherNet/IP协议任然使用TLS1.2版本,为了提高安全性,在今后发展中必然会选择嵌入TLS1.3来提高EtherNet/IP协议的整体安全性。本文使用使用CPN Tools形式化分析工具对TLS1.3握手协议进行建模,模型实现了TLS1.3握手协议的随机数生成、协议版本选择、预主密钥传输和双方身份认证模型。为了防止状态空间爆炸问题限制了随机数的范围,并实现了协议中非对称加密和解密过程的建模。2.目前在协议形式化分析方法和协议分析工具选择上存在一定的盲目性,本文分析EtherNet/IP协议的结构和安全属性,综合分析了协议形式化分析方法和协议分析工具的性能之后选择形式化分析工具CPN Tools和Scyther工具分析TLS1.3握手协议的安全属性。验证了TLS1.3握手协议的安全属性符合协议规范。从分析过程和结果上比较了两种分析工具的性能,CPN Tools在复杂协议分析上具有细化协议内容,更加详细的模拟协议全貌的优势。3.TLS协议是保证网络传输安全的重要标准协议,实现数据加密和数据完整性以及身份验证。由于TLS协议的复杂性和身份认证的多样性,本文基于有限域上椭圆曲线密钥交换方式,使用层次着色Petri网(HCPN)的建模方法对TLS1.3握手协议进行建模,并且添加了Delov-Yao攻击模型,分析了对应模型下的状态空间报告。实验结果表明新发布的TLS1.3握手协议预主密钥有良好的机密性,并且身份认证满足协议规范的安全属性要求。使用Scyther工具验证TLS1.3握手协议没有发现攻击,说明了在今后的EtherNet/IP协议中升级TLS协议的迫切性。