基于Spin工具的KDC密钥交换协议的模型检测分析专业:计算机软件与理论学号：2013021453姓名：马海峰指导老师：许道云基于Spin工具的KDC密钥交换协议的模型检测分析2013级计算机软件与理论马海峰20130214531研究背景与验证环境介绍1.1研究背景与KDC密钥交换协议介绍1.1.1研究背景密码协议是以密码学为基础的消息交换协议,其经常运用与计算机通信网络和分布式系统中，运用密码算法来实现密钥分配和身份认证等功能。现在，密码协议已经在计算机领域得到广泛应用，但是，对密码协议的安全性认证和设计依然很困难。它的条件定义为：小系统：参与协议运行的各主体都是唯一的(如一个发送者，一个响应者)，作用也是唯一的，这些主体也都是诚实的，诚实即是它们严格按照协议规定并遵循自己的身份参与协议运行。为了便于理解，引入强安全性破坏和一般安全性破坏的概念。强安全性破坏：即一个诚实的主体相信在协议运行中用到的一个值是仅他和另外诚实主体之间的共享密码，但入侵者知道这个值。一般安全性破坏:一个诚实主体相信在一个完整协议运行中
