| TCP协议的安全性和活性验证 |
| |
| 引用本文： | 陈道喜,陈冬火,张广泉.TCP协议的安全性和活性验证[J].苏州大学学报(医学版),2008,24(1):54-59,64. |
| |
| 作者姓名： | 陈道喜 陈冬火 张广泉 |
| |
| 作者单位： | 苏州大学计算机科学与技术学院,江苏苏州215006 |
| |
| 基金项目： | 江苏省高校自然科学基金
,
重庆市自然科学基金 |
| |
| 摘 要： | 网络协议簇中，传输控制协议TCP是最重要的协议之一，提供面向连接的可靠传输服务．采用Promela描述TCP建立连接和可靠数据传输，并用模型检测工具Spin，验证TCP三次握手协议的安全性与可靠数据传输协议活性的属性．
|
| 关 键 词： | TCP PROMELA Spin 模型检测 |
| 文章编号： | 1000-2073（2008）01-0054-06 |
| 收稿时间： | 2007-07-05 |
| 修稿时间： | 2007年7月5日 |
The verification of the safety and liveness property of TCP |
| |
| Chen Daoxi,Chen Donghuo,Zhang Guangquan.The verification of the safety and liveness property of TCP[J].Journal of Suzhou University(Natural Science),2008,24(1):54-59,64. |
| |
| Authors: | Chen Daoxi Chen Donghuo Zhang Guangquan |
| |
| Institution: | (School of Computer Science and Technology, Suzhou Univ. , Suzhou 215006, China) |
| |
| Abstract: | The Transmission Control Protocol is one of the most important network protocols in the Internet, and it provides a connection-oriented and reliable transport service. This paper describes of the stablishment of a TCP connection and reliable data transport using Promela,and verify the safety property of three-way handshake protocol and the liveness property of reliable data transport protocol by Spin tool of model checking. |
| |
| Keywords: | TCP promela spin model checking |
| 本文献已被 维普 万方数据 等数据库收录！ |
