基于进程代数的Yahalom协议正确性的形式化验证

摘要

通信过程中为了使得通信双方之间的对话过程是安全传输的,在引入可信第三方的基础上,Yahalom协议借助于可信第三方为通信双方分配"好"的会话密钥,利用该共享密钥加密对话内容保证双方对话的安全。Yahalom协议的形式化验证具有很重要的意义。为了使可信第三方在通信双方之间安全地分配会话密钥,文中对通信过程进行理论化形式的验证。文中基于可信平台的随机会话密钥分配过程进行了抽象化的处理,给出了抽象模型中各个实体状态及状态变迁的操作语义描述,建立了Yahalom协议结构化的操作语义并发计算模型,主要通过ACP公理系统对Yahalom协议的状态变迁系统进行了形式化的验证,验证结果表明Yahalom协议系统地展示了期望的外部行为,从理论上证明了基于进程代数的Yahalom协议是可行的。