无线网络能被用于经济、军事、娱乐以及健康相关的许多应用领域，这些应用常常包括敏感信息的监测，例如战场上敌人的移动或者建筑物里人们的位置。因此，在无线网络里，安全是非常重要的。然而，无线网络遭受到许多约束，包括：低计算能力、小存储空间、有限的能量、有限的节点物理保护、动态变化的拓扑结构以及无线通信信道的不安全使用。归因于这些约束，无线网络安全很难达到。因此，本论文聚焦于无线网络安全协议的设计、建模以及验证。　　本文首先陈述无线网络安全基本概念，然后概括性地介绍了3类重要的安全协议，包括安全定位、会议密钥分配机制以及匿名认证协议。　　然后，两个新颖的安全定位机制被提出，它们能够抵御普遍的袭击。这些方法不仅能够很好地消除使得距离减小的袭击，而且能够完全抵御使得距离增大的袭击。另外，这些方法不涉及任何设备相关的参数，从而能够得到更加准确的定位。除此之外，两个有效的会议密钥分配机制被陈述。其中一个是对著名的NEKED协议改进版本的修正，增强其抵御伪造袭击的能力。本文的抵御措施没有增加额外的通信花销，因此仍然是高效率的。另外，本文指出了NEKED协议改进版当中的一个严重的设计漏洞，并进行了有效的修补。另一个是轻量级安全会议密钥分配机制，它是基于Yi等人所提出的机制上的改进。本文修补了他们协议上的安全漏洞。同时，本研究注意到一些高效率的针对无线移动式通信的匿名认证协议最近已经被提出。本文发现这些机制无法抵御重放袭击和伪装袭击。　　在最后,本文提出一种基于Petri网的安全协议建模和验证方法，它可适用于大多数无线网络安全协议。所提出的Petri网模型不仅能够描述安全协议的动态过程，并且能够对协议的正确性进行形式化验证。利用Petri网模型的状态分析来判断不安全状态是否可达，从而指示了安全协议是否能够提供对袭击者的防御。此方法的提出给无线网络安全应用领域的研究者带来了新的视角—利用Petri网形式化建模以及验证安全应用协议（比如：安全定位、安全同步、安全切换等等）。