【摘要】 进程演算通常用来研究交互式反应系统,其中的互模拟方法是用来形式化验证系统属性的重要途径。首先扩展了进程演算中的Spi演算,并将其应用于形式化描述网络安全协议——Kerberos协议的安全属性。为了验证该协议所声称的安全属性,引入了Spi演算中环境敏感互模拟的方法,即两个系统与环境发生交互过程中是否互模拟。通过采用该互模拟关系对Kerberos协议两个安全属性——可认证性和保密性——的证明,发现其可认证性是可靠的,而保密性存在一个可能的漏洞。最后,指出了基于互模拟的安全协议形式化验证方法今后值得进一步研究的方向。更多还原

【Abstract】 Process calculus is usually used to reason about reactive systems, in which bisimulation method is an important way to formally verify the properties of a system. Firstly, the Spi calculus of process calculus is extended and then used to formally describe the properties of Kerberos protocols, a security protocol. In order to check the claimed security properties, an environmental sensitive bisimulation is introduced for the Spi calculus, which means two bisimulated systems must interact with their environments. Bisimulation proofs on this protocol’s two security properties reveal that the authenticity property holds while its secrecy property is threatened by a possible attack. Finally, the research trend of bisimulation-based formal verification method of security protocols is pointed out.更多还原