论文部分内容阅读
探讨了将串空间模型应用于描述安全协议公平性的方法，并提出串空间模型描述公平协议的一些问题。分析了在描述公平协议时，串空间模型需要进行的几个扩展，包括：描述协议步骤在什么情况可以执行的扩展；描述协议执行过程中角色动态分配的扩展；描述协议步骤同步执行的扩展。应用扩展后的串空间模型对KM协议进行了形式化描述。