Formal Specifications and Verification of a Secure Communication Protocol Model

This paper presents a secure communication protocol model-EABM, by which network security communication can be realized easily and efficiently. First, the paper gives a thorough analysis of the protocol system, systematic construction and state transition of EABM. Then , it describes the channels and the process of state transition of EABM in terms of ESTELLE. At last, it offers a verification of the accuracy of the EABM model.

安全通信协议模型EABRA的设计

提出了一种安全的通信协议模型EABRA，通过该模型可以简单有效地实现网络安全通信。首先对EABRA协议系统、体系结构以及状态转换进行了细致的阐述，然后用ESTELLE语言对协议模型的实现过程进行了具体的描述，最后对EABRA协议模型进行了正确性验证。