论文部分内容阅读
安全协议对手机银行系统的安全性质起着决定作用，是系统成败的关键。对其进行精心的设计和完善的分析是手机银行系统开发中必不可少的一个组成部分。但目前很多手机银行系统中只是简单的使用了若干密码算法作为安全措施，没有把消息交换过程抽象描述成安全协议的形式，更谈不上对其进行形式化的分析证明。密码算法的选择和使用过程也不能为用户提供足够的安全信心。而且整个系统没有充分考虑所有可能的攻击，尤其是重放攻击。 为此，本文深入研究了手机银行的运行环境，安全协议的设计和分析方法及协议所需密码算法的安全性质，精心选择了一套包括分组密码、公钥密码、Hash函数和数字签名的密码算法。在此基础上提出了一个手机银行安全协议-MB协议，分析了设计协议时使用的重要技术，并和其他相关协议进行了比较。 然后基于Strand空间模型给出了其严谨周密的正确性证明。MB协议的正确性主要体现在两个方面：认证属性：当协议主体以某参数完成协议后，被认证主体也必须以该参数参与协议运行。秘密属性：保护协议消息不会泄漏给未被授权的主体。需要指出的是：基于Strand空间理论的正确性证明是建立在已知攻击集的基础上的。 接着使用Kailar逻辑证明了其可追究性，虽然基于逻辑的证明只是满足协议安全目标的必要条件，但该证明的给出可以显著增强使用MB协议的信心。然后分析了该协议抵抗重放攻击的能力和运行效率。最后实现了使用该协议的手机银行原型系统。从协议的分析过程和原型系统运行情况中得到的结论是：MB协议实现了其安全目标，能抵抗目前已知的攻击，且运行性能较优。 本文所做的工作有以下几点： ● 深入研究了常见密码算法的数学基础、基本原理和安全性质，以及选择该算法实现手机银行安全协议的原因。深入研究了安全协议的概念、性质、常用的设计和分析方法，并详细描述了Kailar逻辑和代表安全协议形式化分析发展方向的Stand空间模型(Strand Space Model,SSM)理论。 ● 参照安全协议设计准则，根据手机银行实际运行环境的特点，设计了一个手机银行安全协议，分析了协议中使用的重要技术，并和其他相关协议进行了比较。 ● 使用SSM理论和Kailar逻辑证明了该协议的安全性质。 ● 基于J2ME平台，利用手机模拟器，实现了使用该协议的手机银行原型系统。