中文摘要：

为分析和验证JFKi协议的相关属性,对Spi演算的扩展进行研究,利用扩展Spi演算对JFKi密钥交换协议进行形式化分析,证明JFKi协议满足认证性和保密性。然而,JFKi协议在遭到重放攻击后,发起方的身份信息会泄露,且JFKi协议本身的属性让它更容易遭受Dos攻击。针对这些缺陷,提出一种JFKi协议的改进方案,采用Spi演算验证该方案是可行的且安全性更高。

英文摘要：

To analyze and verify the correlation properties of JFKi protocol, the extension of the Spi calculus was studied and the JFKi key exchange protocol was analyzed using the extended Spi calculus. It was proved that the JFKi protocol could satisfy the authentication and confidentiality. However, the JFKi protocol sponsor＇s identity information may be leaked in the replay at-tack, and the JFKi protocol makes itself more vulnerable to Dos attacks. Aiming at these flaws？ an improved scheme of JFKi protocol was proposed. Through Spi calculus verification, the proposed protocol shows its feasibility and high security.