随着计算机网络技术的发展与应用,网络协议日益复杂,协议开发过程中任何一点错误都将给分布式系统的稳定性、可靠性、坚固性、安全性、容错性以及异种系统之间的互通性带来巨大的危害。因此网络协议的安全性分析和检测就显的极为重要，并且成为当今计算机安全领域中研究的重大课题。　　网络协议一般分为不同层次进行开发，每一层负责不同的通信功能。数据链路层是一切数据通信网络最基础的架构，也是一切高层协议赖以实现的基础。因此数据链路层协议的安全性对整个网络通信起的至关重要的作用。　　采用形式化方法(formalmethds)之一的模型检测技术对网络协议进行形式化验证和分析，是构建一个可靠协议的重要途径。国外研究者Lesilie Lamport提出了一种新逻辑，行为时序逻辑（TLA）理论体系，运用这种逻辑对协议进行建模，在一度程度上可以减少由于状态空间爆炸带来的压力。用TLA描述和推理并发系统，结合了标准时序逻辑和动作逻辑的特点，具有较强的描述和推理能力。基于TLA的系统描述语言TLA+以模块的形式构造规约，并通过扩展和实例化等方法把多个模块组合以形成更为复杂的规约。用这种方法取得的模块式规约可以通过TLA的检测工具TLC来检测，检验目标属性是否符合规约并举出反例。因此，不论在理论上还是在实际应用中，这种模型检测技术都具有一定的研究价值。　　本文在在详细介绍数据链路层基本协议及其工作原理的基础上，分析了行为时序逻辑基本理论，运用基于行为时序逻辑TLA的规约语言TLA+与模型检测工具TLC对协议进行分析与检测，所作的主要工作与创新之处如下：　　对数据链路层中的停止等待ARQ协议,连续ARQ协议的算法以及滑动窗口协议作了深入分析。根据ARP协议工作原理，找出ARP协议弱点，结合ARP攻击的主要方式给出应对措施。　　根据ARP报文格式和Libnet构造数据包的流程即初始化libnet_init()——构造ARP协议块——构造以太网协议块——发送数据包——销毁libnet_destroy的过程构造ARP应答数据包。在构造ARP应答数据包时将源主机的MAC地址填充成其他主机的MAC地址即可以实现ARP欺骗。　　对Leslie Lamport提出的行为时序逻辑（Temporal Logic of Action）作较为全面的研究,对TLA中基本概念如变量、状态函数、使能谓词，以及TLAII中的活性，公平性等概念进行深入研究。在对公平性的研究中得出强公平性可以推出弱公平性的结论。　　分析行为时序逻辑理论，利用一个拥有三个字段的记录构造网络通信通道chan，三个字段中有一个字段代表通道中传送的内容，另两个字段的值是0或1，它们用于保证通道在使用过程中传输的同步性。在发送者和接收者之间加入一个缓冲区，然后在发送者与缓冲区以及缓冲区与接收者之间分别加入一个通道chan就可以实现消息的异步传输。在通道设计的过程中的每一步，文中都给出了具体的实例及使用方法。　　研究基于行为时序逻辑TLA的描述语言TLA+和模型检测工具TLC的检测原理及建模要求。将待规约的系统或协议表示成TLA+的标准形式而后用TLC进行检测。在规约中加入THEOREM Spec=>Property，就可以检验属性Property是否满足模型Spec所描述的系统。若不满足则会给出一条路径，这条路径也就是属性不满足系统的一个反例。　　根据停止等待ARQ协议的算法，用TLA+对ARQ协议进行建模。用TLC验证了ARQ协议应该满足的两条基本属性，其中一条属性如：A给B发送出数据帧后,B最终一定能收到A发来的数据帧，得到的结果是正确、错误或重复的数据帧。根据ARQ协议的弱点，在协议中加入一个攻击者Intuder，攻击者截获接收者发送来的ARQ应答，造成ARQ拒绝服务攻击。　　根据同一网段ARP协议的算法，用TLA+构造一个ARP协议模型，在协议中构造了一个攻击者行为造成ARP欺骗。用TLC验证后得到一个攻击者的攻击路径。