安全协议的验证是网络安全研究中的热点和难点，本文把局部可操作函数引入到实例空间协议分析方法中，简化了协议的描述和分析，增强了实例空间方法的可扩展性，并用新的理论框架分析了JFKi和JFKr协议核心部分的两个安全性质。JFK协议是新近提出的以代替IKE协议为目标的密钥交换协议，它提供很多安全服务，分析它的安全性具有很高的研究和应用价值。本文证明了JFKi协议核心部分满足相互认证性和协商密钥秘密性，而JFKr协议核心部分只保证协商密钥的秘密性。 本文首先提出一个引进局部可操作函数的消息交换模型作为协议的执行模型。局部可操作函数用于表示主体对消息的操作，包括联接、分解、加密、解密、签名、Hash计算等，代表了主体的能力。引入局部可操作函数后，消息交换模型的分析函数如Poss、Sees等的定义更为简单，而更重要的是，它们的描述能力更强。另外，本文还证明了扩展的消息交换模型的很多定理。接着本文介绍了引入局部可操作函数项的与消息交换模型相对应的协议描述模型，并重新定义了它们之间的关联函数——实例函数。在实例函数的基础上本文定义了实例空间并证明了很多关于实例空间原子命题的性质，其中有不少是引入局部可操作函数后增加或修改的。这些性质和消息交换模型中的定理都是我们分析协议安全性的关键。其中最为重要的是(n，1)-SecrecyProperties，本文利用局部可操作函数的概念重新定义了消息泄漏和获取函数，并重新证明了(n，1)-SecrecyProperties。最后本文利用这个扩展了的实例空间协议分析方法结合可观察理论分析了JFKi和JFKr协议核心部分的相互认证性和协商密钥秘密性，并在分析证明过程中讨论了实例空间分析方法如何体现一个协议可能存在的冒充攻击，间接增强了这一方法分析协议的可靠性。