数字签名过程的一个形式描述和验证

通过引入一些新概念,利用Biba模型思想,对一般的数字签名方案形式化描述和验证,并且该模型具有完整性.

一种新的动态指配光网络资源的接口信令协议

本文提出了一种新的用户光网络接口 (UNI)信令协议 ,以实现动态指配光网络资源的功能 .该协议支持多种类客户寻址 ,考虑了光网络的特殊要求 .采用通信有限状态机 (CFSM)模型对协议进行了形式化描述和验证 ,分析了协议设计的出错处理 .分析和验证结果表明 ,协议在网络正常和超时故障条件下均能确保对光通道的建立、修改、拆除和查询等操作无误 ,具有无死锁、无活锁。