Internet安全会话解析和一个简单模型的正确性分析

AN ANALYSIS OF INTERNET SECURE SESSION AND THE PROVING OF A SIMPLIFIED MODEL

本文简单分析了因特网上典型安全会话过程。首先介绍了安全会话的基本要求和一些常用技术，然后分析了一个典型对话握手过程，最后用 Ｕ Ｎ Ｉ Ｔ Ｙ 对其进行规范描述和正确性分析。

This article gives a simple analysis of a typical secure session on the Internet. First it briefly describes the requirement and some technologies used. Then an analysis of typical session handshaking follows. At last, a formal description is given and the correctness is proved with UNITY.