一种应用层安全通信协议的形式描述和验证

安全通信是一个日益重要的问题。本文作者在［１］中在应用层设计了一个安全通信控制设备（ＳＣＣＭ），来实现安全通信。本文用ＡＳＮ．１对此安全通信协议的协议数据元进行描述，然后根据协议状态转移图、应用可达性分析技术来验证协议的完整性、无死锁、无活锁、终止性等重要性质。