CSP方法分析与改进移动自组织网络TAM认证协议

"该文主要讨论了基于CSP方法对移动自组织网络认证协议TAM的分析与改进，旨在解决认证协议在应对安全威胁和实现安全目标上的有效性问题。研究者通过CSP模型和模型检测工具FDR对TAM协议进行建模、验证，并提出改进方案。" 在移动自组织网络(MANET)中，认证协议是确保网络安全的关键，它们用于验证节点间的通信合法性，防止恶意攻击。TAM是一种代表性的MANET认证协议，但其在面对特定安全挑战时可能存在不足。本文作者刘礼才、殷丽华、郭云川和孙燕采用通信顺序进程(CSP)这一形式化方法，对TAM协议进行了深入分析。 CSP是一种强大的建模语言，用于描述并发系统中不同组件之间的通信行为。在该研究中，CSP被用来建模TAM协议中的参与者行为，同时定义了与安全目标相符的安全规范。这些规范包括认证性（确保消息来源的可靠性）和机密性（保护信息不被未授权的第三方获取）。 利用FDR（Fairness for Dummies and Realists）模型检测工具，研究人员对TAM的CSP模型进行了检验。FDR能够检查协议是否满足预定义的安全属性。结果显示，原始的TAM协议在认证性和机密性方面存在缺陷，即不满足CSP进程中的安全规范。 针对这些问题，研究团队对TAM进行了改进，设计了新的通信流程和安全机制。经过改进后的TAM通过了模型检测，表明它现在能够满足既定的安全目标。实验对比表明，尽管改进的TAM在一定程度上增加了计算和通信开销，但在合理的簇规模下，这些额外开销是可接受的，从而确保了整体安全性能的提升。 该研究强调了形式化方法在评估和改进安全协议中的重要性，尤其是对于MANET这样动态、去中心化的网络环境。通过对TAM的分析和改进，研究不仅提高了协议的安全性，也为未来MANET认证协议的设计提供了参考和指导。 关键词: 移动自组织网络、认证协议、安全协议分析、通信顺序进程、TAM 中图分类号: TP309 文献标识码: A 文章编号: 1000-436X(2013)Z1-0058-09