ARP协议的描述与TLA验证

• 作者: 吴勇 李元 李祥
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: ARP协议 ARP欺骗 行为时序逻辑
• 年，卷（期）: 2010,（6）
• 所属期刊栏目: 安全与防范
• 页码范围: 163-166
• 分类号: TP393.08
• 字数: 2439字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2010.06.042

摘要

随着计算机网络的发展,网络的安全性日益受到人们的关注.ARP攻击是一种非常专业化的网络攻击方式,它会给网络管理员增加很大的负担,破坏主机数据,窃取主机信息.Lesilie Lamport提出了一种新的逻辑,即行为时序逻辑(TLA)理论体系,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达程序与属性.文中介绍了ARP协议,用基于行为时序逻辑TLA的建模语言TLA+对ARP协议进行建模分析.构造了一个ARP欺骗的攻击者模型,用基于TLA的模型检测工具TLC对其进行验证并找出一条攻击者路径.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李祥	贵州大学计算机软件与理论研究所	91	551	13.0	19.0
2	李元	贵州大学计算机软件与理论研究所	7	9	2.0	3.0
3	吴勇	贵州大学计算机软件与理论研究所	2	4	1.0	2.0