无线体域网(Wireless Body Area Network)是一个附着在人体上的微型网络。无线传感器加入无线体域网后,医生与患者可以实时远程监控患者的生理数据。例如心跳、血压、胰岛素水平和呼吸等,为实现医疗服务行业中的智能操作、智能管理、智能监控提供了可能。然而无线传输的开放性导致患者生理数据在传输过程中容易受到非法者未经授权的访问和修改,造成隐私泄露、非法监听、数据篡改等信息安全问题,而这些操作可能会对患者产生不可逆的损害。本文重点关注无线体域网环境下的三方认证协议的认证性以及一致性,分别选取基于NTRU、3PAKE、ECDH三种密码体制的三方认证协议作为研究对象,采用形式化方法分析无线体域网环境下三方认证协议的安全性,研究成果如下:(1)基于Maggi的Promla建模方法,构建攻击者二次重放消息的能力。分别使用模型检测方法分析基于3PAKE、ECDH和NTRU密钥体制的三方认证协议,证明了模型检测方法的通用性,并成功发现基于3PAKE和基于NTRU密钥体制的三方认证协议存在Dos攻击漏洞。(2)分析基于3PAKE和NTRU密钥体制的三方认证协议存在攻击漏洞的原因,提出协议改进方法,并验证改进后协议的安全性。模型检测验证结果表明改进后的三方认证协议安全性更高,能够有效抵御Dos攻击漏洞;总结本文所研究的不同密钥体制下三方认证协议存在的安全隐患。(3)提出一种分类压缩的建模优化策略,对比采用语法重定序、偏序规约、类型检查、分类压缩优化策略后模型的状态迁移量等数据,实验结果表明加入分类压缩优化策略后能够有效缓解状态爆炸问题。