一种新的类BAN逻辑模态语义模型——兼论类BAN逻辑的语法缺陷

由于类BAN逻辑缺乏明确而清晰的语义，其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型，在此基础上定义了符合模态逻辑的类BAN逻辑“可能世界”语义模型，并从语义的角度证明了在该模型下的类BAN逻辑语法存在的缺陷，同时，指出了建立或改进类BAN逻辑的方向。

On Semantics Model of BAN-like Logic and Flaws in its Syntax Rules

For lack of explicit and definite semantics in BAN like logics, their correctness of syntax rules and reasoning is under suspicion. In this paper, a computing model for security protocols is defined. Based on it, semantics model about possible word of BAN like logic is defined conforming with traditional modal logic. And from the viewpoint of semantics, some syntax flaws in BANrlike logic are proved. Also, how to construct a new logic or improve BAN-like logics is pointed out.