一种理性安全协议的博弈逻辑描述模型

博弈逻辑ＡＴＬ和ＡＴＥＬ可以对传统安全协议的公平性、安全性等性质进行分析与验证。但在理性环境中，由于参与者对知识的自利性，ＡＴＬ和ＡＴＥＬ都不能形式化分析与验证理性安全协议。因此在ＣＥＧＳ中引入效用函数和偏好关系知识，得到新的ｒＣＥＧＳ，并在合作模态算子《Γ》中加入行为ＡＣＴ参数，提出新的可形式化分析理性安全协议的交替时序认知逻辑ｒＡＴＥＬ－Ａ。然后运用ｒＡＴＥＬ－Ａ构建两方理性安全协议的形式化模型，并基于ｒＣＥＧＳ的等价扩展式博弈，对具体的两方理性交换协议进行形式化分析，结果表明构建的形式化模型可以有效地形式化分析理性安全协议的正确性、理性安全性和理性公平性。