论文部分内容阅读
本文研究了SSL协议的协议栈结构，重点分析了SSL3.0安全协议中的握手过程。在此基础上，基于CSP(Communicating Sequential Processes)理论建立了SSL3.0安全协议的形式化模型，对SSL3.0安全协议中的握手过程进行了精确的描述。
Spi演算是基于Pi演算的子演算，专门用于描述和分析基于密码学的安全协议。本文介绍了Spi演算的基本概念，以及如何基于Spi演算对安全协议进行分析。基于此，本文针对SSL3.0安全协议握手过程中的三种认证模式分别建立了Spi演算形式化模型，详细分析了SSL安全协议的握手过程，论证了SSL3.0安全协议的认证性。并且针对各种攻击，本文结合形式化模型分析了SSL协议是如何抵御攻击的。最终，本文根据基于Spi演算的形式化模型，找到了SSL握手协议中存在的冗余，并提出了对SSL协议改进，对以后的研究进行了展望。
本文基于进程演算对SSL安全协议进行的形式化分析，有助于对SSL安全协议的深入理解，为SSL安全协议的设计和改进提供了坚实的基础。并且对于安全协议的研究具有一定的借鉴意义。