随着信息技术的发展，计算机网络正以惊人的速度向各个领域渗透，它帮助人们可以在虚拟世界里从事越来越多的复杂活动。然而，网络在为人们提供便捷生活的同时，其带来的安全问题也越来越突出。网络协议作为一种规范，在确保网络安全环境的同时，还在不同的层面细致地规定了参与者之间的行为，同时定义了交互过程中数据传输的类型和格式。因此，如何保证网络协议在遭受攻击时仍然可以安全、正确的运行，一直都是很大的挑战。针对这一问题，研究者们提出了利用形式化方法来对协议进行分析，并逐渐划分为三种类别:形式化逻辑方法、模型检测方法和定理证明方法。但遗憾的是目前的研究工作大都集中于前两者。　　基于此，本文采用了一种基于定理证明的形式化方法，完成了对数据链路层传输协议以及Needham-Schroeder认证协议的形式化分析，同时在Rodin系统中完成了相关的模型与实验。　　本文所作的工作主要体现在以下几个方面:　　(1)利用Event-B方法对数据链路层的滑动窗口传输协议完成了分析;　　本文从一个理想信道上运行的滑动窗口协议开始，利用Event-B实现其模型并通过一系列的证明保证了协议目标的正确可达;随后在此基础上，引入了错误处理及重传机制，完成了在有噪信道中传输的滑动窗口协议的分析;　　(2)利用Event-B方法对网络安全领域著名的Needham-Schroeder协议及其修正的安全性完成了分析;　　本文首先完成了朴素的Needham-Schroeder协议的分析，验证了其可以达成预期的认证目标;接着针对其在重放攻击下失效的缺陷，对一种修改进行了形式化的分析，证明了即使在重放攻击下，协议预期的认证目标仍然能够达成。