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