基于形式化模型的电力信息审计系统安全协议验证方法

摘要

由于已有方法未能使用形式化模型,导致安全协议验证效率下降,安全协议验证错误率和开销增加。结合形式化模型,提出一种基于形式化模型的电力信息审计系统安全协议验证方法。通过形式化模型,对电力信息审计系统进行形式化研究,采用SPIN和AVISPA对电力信息审计系统安全协议进行改进。利用Promela和HLPSL进行建模,查找安全协议中存在的攻击,获取攻击者的相关信息,查看存在的漏洞,完成电力信息审计系统安全协议验证。仿真实验结果表明,所提方法能够有效提升安全协议验证效率,降低安全协议验证错误率和开销。