中文摘要：

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

英文摘要：

An SDL design model of security-critical product is analyzed, the state transition process ofan exchange ofkey encryption key is illuminated, and some problems are discussed involved in analysis, simulation and validation of the model using tools. By the example, the application process of formal techniques is narrated in engineering, especially in security-critical system. The outstanding characteristic is analyzed the exchange of key encryption key and obtaining its framework by applying SDL, validating the framework using bit state exploration algorithm.