论文部分内容阅读
分析了一个信息安全产品的SDL设计模型，说明了密钥加密密钥交换的状态迁移过程，讨论了在使用SDL分析工具对模型进行分析、模拟、验证甚至代码生成中涉及的一些问题。通过实例分析，说明了形式化技术在工程中特别是安全系统的设计开发过程中的应用过程。特点是运用SDL，分析得出了密钥加密密钥交换的框架结构，并使用比特状态探测算法对其进行了验证。