面向协议安全性质的形式化协同规约方法及图形建模系统

摘要

本发明公开了一种面向协议安全性质的形式化协同规约方法，涉及可信软件和通信协议技术领域。所述方法包括：面向计算树逻辑(Computation Tree Logic，CTL)和不变性(Invariant)的软件功能安全性质(Safety Property)规约规范；针对机密性(Confidential)、认证性(Authenticity)、完整性(Integrity)和可用性(Availability)的信息安全性质(Security Property)规约规范。本发明中，通过约定这些规约规范能够较为全面地针对协议的行为和内容对功能安全性质和信息安全性质建模，为后续的验证提供一定的帮助，能够为建模用户和性质的形式化验证器建立有效的连接桥梁，节约协议标准的开发和验证的时间和成本。