| ARP协议的描述与TLA验证 |
| |
| 引用本文： | 李元,吴勇,李祥. ARP协议的描述与TLA验证[J]. 计算机技术与发展, 2010, 20(6): 163-166 |
| |
| 作者姓名： | 李元 吴勇 李祥 |
| |
| 作者单位： | 贵州大学,计算机软件与理论研究所,贵州,贵阳,550025 |
| |
| 基金项目： | 美国GeneChiu基金 |
| |
| 摘 要： | 随着计算机网络的发展,网络的安全性日益受到人们的关注.ARP攻击是一种非常专业化的网络攻击方式,它会给网络管理员增加很大的负担,破坏主机数据,窃取主机信息.Lesilie Lamport提出了一种新的逻辑,即行为时序逻辑(TLA)理论体系,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达程序与属性.文中介绍了ARP协议,用基于行为时序逻辑TLA的建模语言TLA+对ARP协议进行建模分析.构造了一个ARP欺骗的攻击者模型,用基于TLA的模型检测工具TLC对其进行验证并找出一条攻击者路径.
|
| 关 键 词： | ARP协议 ARP欺骗 行为时序逻辑 |
The Description and Validation of ARP Protocol Based on TLA |
| |
| LI Yuan,WU Yong,LI Xiang. The Description and Validation of ARP Protocol Based on TLA[J]. Computer Technology and Development, 2010, 20(6): 163-166 |
| |
| Authors: | LI Yuan WU Yong LI Xiang |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
