移动Ad Hoc网络安全路由协议设计与分析技术研究
|
摘要
移动Ad Hoc网络（Mobile Ad Hoc Networks，MANETs）是一种无基础设施的多跳无线网络，网络节点既是主机又是路由器，只有依赖网络中所有可信节点协作，安全路由协议才能获得可信路径信息，而这种“依赖”需借助密码学安全协议实现。然而，在分析路由协议安全性时，与分析密码学安全协议安全性不同，必需考虑构成路径的网络中间节点行为。因此，用于密码学安全协议的形式化分析技术不能直接用于安全路由协议的安全分析，设计分析安全路由协议的新方法具有重要的理论和应用价值。
目前广泛使用的针对密码学安全协议的形式化分析模型可分为两大类：计算模型和符号模型。本论文针对移动Ad Hoc网络路由协议安全分析的特殊性，基于两种流行的密码学安全协议安全分析技术-通用可复合UC（Universally Composable）安全计算模型和协议复合逻辑PCL（Protocol Compisition Logic）符号模型，研究了以下几个方面的内容：
第一，路由安全威胁模型的研究。本论文分析了现有路由安全威胁模型active-n-m攻击模型、参数化威胁模型、自适应威胁模型等存在的问题，基于Dolev-Yao攻击模型并综合现有威胁模型的特点，提出了更加适合于建模路由安全威胁的层次化威胁模型。
第二，基于UC安全理论的路由安全分析技术研究。针对多路径距离矢量路由安全分析问题，基于层次化威胁模型和攻陷网络拓扑模型，提出了多路径距离矢量路由协议安全需求-可信系统状态概念，并给出了多路径距离矢量路由协议理想函数及安全定义，对基于UC安全理论的路由安全分析模型UC-RP（UC for RoutingProtocol）模型作了进一步的补充和完善。
第三，基于PCL的路由安全分析技术研究。PCL是一种用于分析密码学安全协议，如认证协议、密钥协商协议等的符号模型。本论文引入线程位置和线程位置相邻概念，扩展PCL提出了建模移动Ad Hoc网络和分析路由协议安全性的符号模型PCL-RP(PCL for Routing Protocol)模型。PCL-RP模型把移动Ad Hoc网络模型化为不同逻辑位置上运行的线程复合，用线程邻居集及邻居集的变化描述多跳无线网络的动态拓扑关系，用广播规则模型化多跳无线网络广播通信特征，用符号迹概念模型化路由协议执行过程，提出网络迹概念模型化符号迹上事件导致的网络进化过程，在网络迹上定义了PCL-RP模型中谓词公式和模态公式的语义，提出了路由协议安全分析的新方法。
第四，路由协议通用可复合符号分析技术研究。PCL-RP模型协议符号分析比UC-RP模型协议分析简单、直观并且易于实现自动化分析。然而，PCL-RP模型中的符号分析缺乏计算可靠性。借鉴密码学安全协议计算可靠性符号分析的最新研究成果，本论文融合UC-RP模型和PCL-RP模型，提出了路由协议通用可复合符号分析模型UCSA-RP（Universally Composable Symbol Analysis for RoutingProtocol）模型，在UCSA-RP模型中说明了如何用PCL-RP模型的符号分析方法断言UC-RP模型中的协议安全性。
第五，多路径安全路由协议的设计与分析技术研究。AMR（AggregateMulti-paths Routing）算法是计算节点不相交多路径路由的累积多路径路由机制，本论文整合AMR算法和单路径距离矢量路由协议AODV协议，引入密码学安全机制、错误检测机制和路径确认机制，设计了节点不相交多路径距离矢量安全路由协议SMDVR（Secure Multi-paths Distance Vector Routing），并在UC-RP模型中分析了SMDVR协议的安全性，SMDVR协议的可证明安全性能够归约为签名机制的安全性。另外，对SMDVR协议与相关协议方案的效率作了比较分析。
第六，编码感知安全路由协议的设计与分析技术研究。本论文研究了全局网络编码系统DCAR(Distributed Code-Aware Routing)存在的问题，提出了适合于编码感知安全路由协议的安全目标，基于DCAR，设计了编码感知安全路由协议DCASR(Distributed Code-Aware Secure Routing)，并在PCL-RP模型中建模并分析了DCASR协议的安全属性，证明新协议能够满足本论文提出的安全目标。在UCSA-RP模型中证明PCL-RP模型中DCASR协议的符号安全准则蕴含UC-RP模型中的计算安全定义，说明了DCASR协议的计算可靠性。
Mobile ad hoc networks (MANETs) are collections of wireless mobile devices withrestricted broadcast range and resources, are multi-hop wireless network without fixedinfrastructure. These networks are decentralized, with nodes acting both as hosts androuters, forwarding packets for nodes that not in transmission range of each other.Secure routing can obtain information of trusted routing only depend on incorporatingbetween honest nodes. Implement of this “dependence” need to resort to somecryptographic primitives to establish integrity authentication of routing informationand to provide entity authentication between honest nodes. However, difference withsecurity analysis of cryptographic protocol, we must consider behavior of networkintermediate nodes that form routing. Therefore, formal analysis technologies forsecure protocol can’t be directly used for security verification of routing. We mustdevelop new formal approaches of security analysis of routing for mobile ad hocnetworks.
Two families of popular models have been designed for the rigorous analysis ofsecurity protocols: the so-called symbolic models (Dolev-Yao, formal) on the one handand the computational (cryptographic, concrete) models on the other hand. In thisdissertation, aim at the particularity of routing security analysis for mobile ad hocnetworks, we study theories and approaches of routing security analysis in UC(Universally Composable) model that is a computational model of security analysis ofcryptographic protocols and PCL (Protocol Composable Logic) that is a symbolanalysis model. The main results presented are as follows:
1.Correct representation of security threat model of routing is basis of securityanalysis of routing. In this dissertation, we firstly analysis issues of existingsecurity threat model, such as active-n-m attacker model, the parametric attackermodel and the adaptive attacker model. Based on existing security threat model ofrouting and Dolev-Yao threat model, we propose a new threat model-thehierarchical threat model.
2. UC-RP (UC for Routing Protocol) model based on UC theory is latest approachof routing security analysis. In this dissertation, aim at analysis issue ofdevelopment and analysis of multi-paths distance vector routing, the concept oftrusted system state is proposed. Trusted system state is security requirement of multi-paths distance vector routing. The ideal functionality is given and securitydefinition is proposed. We further complete and improve UC-RP model.
3.PCL is a symbol model for reasoning about security properties for cryptographicprotocols such as authentication protocols and key agreement protocols etc. Inthis dissertation, we extend PCL and propose a PCL-RP (PCL for RoutingProtocol) model to model mobile ad hoc networks and analysis security of routing.In PCL-RP, the concepts of location and neighboring location of thread areintroduced. The dynamic topology of multi-hop wireless networks was describedby the set of neighbors for threads. The broadcast rule of neighboring locationthreads models the feature of wireless broadcast communication. Symbol traceproposed models execution process of routing and network trace proposed in thisdissertation models network evolution that resulted from events on symbol trace.The semantics of predicates and modal formula are defined and security ofrouting is analyzed on network trace.
4.Symbolic analysis of PCL-RP is dramatically simpler than full-fledgecryptographic analysis of UC-RP. In particular, it is readily amenable toautomation. However, symbolic analysis does not a priori carry anycomputational soundness guarantees. Following recent work on computationalsound symbolic analysis, we propose UCSA-RP (Universally ComposableSymbol Analysis for Routing Protocol) by reconciling UC-RP and PCL-RP. Wedemonstrate how symbol analysis of PCL-RP can be used to assert the security ofrouting within UC-RP.
5.The algorithm of AMR (Aggregate Multi-paths Routing) is a routing mechanismthat computes the maximal set of node-disjoint paths. In this dissertation,integrating the algorithm of AMR and AODV, we develop multiple node-disjointpaths secure distance vector routing (SMDVR), and security of SMDVR isanalyzed in UC-RP. It is proved that the security of SMDVR can be reduced tothe security of the digital signature.
6.In this dissertation, we firstly study issues in DCAR (Distributed coding-AwareRouting) and propose a new security destination that is fit for coding-awaresecure routing. And then, based on DCAR, we develop a secure routing DCASR(Distributed Coding-Aware Secure Routing). We model DCASR and analysissecurity properties in PCL-RP. It is proved that DCASR can satisfy our securitydestination. In UCSA-RP, We show that DCASR satisfies symbolic securitycriterion in PCL-RP if and only if the corresponding cryptographic protocol is secure in UC-RP.
目前广泛使用的针对密码学安全协议的形式化分析模型可分为两大类：计算模型和符号模型。本论文针对移动Ad Hoc网络路由协议安全分析的特殊性，基于两种流行的密码学安全协议安全分析技术-通用可复合UC（Universally Composable）安全计算模型和协议复合逻辑PCL（Protocol Compisition Logic）符号模型，研究了以下几个方面的内容：
第一，路由安全威胁模型的研究。本论文分析了现有路由安全威胁模型active-n-m攻击模型、参数化威胁模型、自适应威胁模型等存在的问题，基于Dolev-Yao攻击模型并综合现有威胁模型的特点，提出了更加适合于建模路由安全威胁的层次化威胁模型。
第二，基于UC安全理论的路由安全分析技术研究。针对多路径距离矢量路由安全分析问题，基于层次化威胁模型和攻陷网络拓扑模型，提出了多路径距离矢量路由协议安全需求-可信系统状态概念，并给出了多路径距离矢量路由协议理想函数及安全定义，对基于UC安全理论的路由安全分析模型UC-RP（UC for RoutingProtocol）模型作了进一步的补充和完善。
第三，基于PCL的路由安全分析技术研究。PCL是一种用于分析密码学安全协议，如认证协议、密钥协商协议等的符号模型。本论文引入线程位置和线程位置相邻概念，扩展PCL提出了建模移动Ad Hoc网络和分析路由协议安全性的符号模型PCL-RP(PCL for Routing Protocol)模型。PCL-RP模型把移动Ad Hoc网络模型化为不同逻辑位置上运行的线程复合，用线程邻居集及邻居集的变化描述多跳无线网络的动态拓扑关系，用广播规则模型化多跳无线网络广播通信特征，用符号迹概念模型化路由协议执行过程，提出网络迹概念模型化符号迹上事件导致的网络进化过程，在网络迹上定义了PCL-RP模型中谓词公式和模态公式的语义，提出了路由协议安全分析的新方法。
第四，路由协议通用可复合符号分析技术研究。PCL-RP模型协议符号分析比UC-RP模型协议分析简单、直观并且易于实现自动化分析。然而，PCL-RP模型中的符号分析缺乏计算可靠性。借鉴密码学安全协议计算可靠性符号分析的最新研究成果，本论文融合UC-RP模型和PCL-RP模型，提出了路由协议通用可复合符号分析模型UCSA-RP（Universally Composable Symbol Analysis for RoutingProtocol）模型，在UCSA-RP模型中说明了如何用PCL-RP模型的符号分析方法断言UC-RP模型中的协议安全性。
第五，多路径安全路由协议的设计与分析技术研究。AMR（AggregateMulti-paths Routing）算法是计算节点不相交多路径路由的累积多路径路由机制，本论文整合AMR算法和单路径距离矢量路由协议AODV协议，引入密码学安全机制、错误检测机制和路径确认机制，设计了节点不相交多路径距离矢量安全路由协议SMDVR（Secure Multi-paths Distance Vector Routing），并在UC-RP模型中分析了SMDVR协议的安全性，SMDVR协议的可证明安全性能够归约为签名机制的安全性。另外，对SMDVR协议与相关协议方案的效率作了比较分析。
第六，编码感知安全路由协议的设计与分析技术研究。本论文研究了全局网络编码系统DCAR(Distributed Code-Aware Routing)存在的问题，提出了适合于编码感知安全路由协议的安全目标，基于DCAR，设计了编码感知安全路由协议DCASR(Distributed Code-Aware Secure Routing)，并在PCL-RP模型中建模并分析了DCASR协议的安全属性，证明新协议能够满足本论文提出的安全目标。在UCSA-RP模型中证明PCL-RP模型中DCASR协议的符号安全准则蕴含UC-RP模型中的计算安全定义，说明了DCASR协议的计算可靠性。
Mobile ad hoc networks (MANETs) are collections of wireless mobile devices withrestricted broadcast range and resources, are multi-hop wireless network without fixedinfrastructure. These networks are decentralized, with nodes acting both as hosts androuters, forwarding packets for nodes that not in transmission range of each other.Secure routing can obtain information of trusted routing only depend on incorporatingbetween honest nodes. Implement of this “dependence” need to resort to somecryptographic primitives to establish integrity authentication of routing informationand to provide entity authentication between honest nodes. However, difference withsecurity analysis of cryptographic protocol, we must consider behavior of networkintermediate nodes that form routing. Therefore, formal analysis technologies forsecure protocol can’t be directly used for security verification of routing. We mustdevelop new formal approaches of security analysis of routing for mobile ad hocnetworks.
Two families of popular models have been designed for the rigorous analysis ofsecurity protocols: the so-called symbolic models (Dolev-Yao, formal) on the one handand the computational (cryptographic, concrete) models on the other hand. In thisdissertation, aim at the particularity of routing security analysis for mobile ad hocnetworks, we study theories and approaches of routing security analysis in UC(Universally Composable) model that is a computational model of security analysis ofcryptographic protocols and PCL (Protocol Composable Logic) that is a symbolanalysis model. The main results presented are as follows:
1.Correct representation of security threat model of routing is basis of securityanalysis of routing. In this dissertation, we firstly analysis issues of existingsecurity threat model, such as active-n-m attacker model, the parametric attackermodel and the adaptive attacker model. Based on existing security threat model ofrouting and Dolev-Yao threat model, we propose a new threat model-thehierarchical threat model.
2. UC-RP (UC for Routing Protocol) model based on UC theory is latest approachof routing security analysis. In this dissertation, aim at analysis issue ofdevelopment and analysis of multi-paths distance vector routing, the concept oftrusted system state is proposed. Trusted system state is security requirement of multi-paths distance vector routing. The ideal functionality is given and securitydefinition is proposed. We further complete and improve UC-RP model.
3.PCL is a symbol model for reasoning about security properties for cryptographicprotocols such as authentication protocols and key agreement protocols etc. Inthis dissertation, we extend PCL and propose a PCL-RP (PCL for RoutingProtocol) model to model mobile ad hoc networks and analysis security of routing.In PCL-RP, the concepts of location and neighboring location of thread areintroduced. The dynamic topology of multi-hop wireless networks was describedby the set of neighbors for threads. The broadcast rule of neighboring locationthreads models the feature of wireless broadcast communication. Symbol traceproposed models execution process of routing and network trace proposed in thisdissertation models network evolution that resulted from events on symbol trace.The semantics of predicates and modal formula are defined and security ofrouting is analyzed on network trace.
4.Symbolic analysis of PCL-RP is dramatically simpler than full-fledgecryptographic analysis of UC-RP. In particular, it is readily amenable toautomation. However, symbolic analysis does not a priori carry anycomputational soundness guarantees. Following recent work on computationalsound symbolic analysis, we propose UCSA-RP (Universally ComposableSymbol Analysis for Routing Protocol) by reconciling UC-RP and PCL-RP. Wedemonstrate how symbol analysis of PCL-RP can be used to assert the security ofrouting within UC-RP.
5.The algorithm of AMR (Aggregate Multi-paths Routing) is a routing mechanismthat computes the maximal set of node-disjoint paths. In this dissertation,integrating the algorithm of AMR and AODV, we develop multiple node-disjointpaths secure distance vector routing (SMDVR), and security of SMDVR isanalyzed in UC-RP. It is proved that the security of SMDVR can be reduced tothe security of the digital signature.
6.In this dissertation, we firstly study issues in DCAR (Distributed coding-AwareRouting) and propose a new security destination that is fit for coding-awaresecure routing. And then, based on DCAR, we develop a secure routing DCASR(Distributed Coding-Aware Secure Routing). We model DCASR and analysissecurity properties in PCL-RP. It is proved that DCASR can satisfy our securitydestination. In UCSA-RP, We show that DCASR satisfies symbolic securitycriterion in PCL-RP if and only if the corresponding cryptographic protocol is secure in UC-RP.
引文
[1] Burrows M, Abadi M, and Needham R. A logic of authentication [J]. ACMTransactions on Computer Systems (TOCS),1990,8(1):18-36.
[2] Fabrega F, Herzog J, and Gurrman J. Strand Spaces: Proving security protocolscorrect [J]. Journal of Computer Security,1999,7(2):191-230.
[3] Backes M, Pfitzmann B, and Waidner M. The reactive simulatability framework [J].Information and Computation,2007,205(12):1685-1720.
[4] Hu Y. C, Perrig A. A survey of secure wireless ad hoc routing [J]. IEEE Security&Privacy,2004,2(3):28-39.
[5] TODD R, Yasinsac A. Surveying Security Analysis Techniques in MANETRouting Protocols [J], IEEE Communications,2007,9(4):69-84.
[6] Bellare M and Rogaway P. Random Oracles are practical: A paradigm fordesigning efficient protocols [C]. In: Proceeding of the1stACM conference onComputer and Communications Security. New York: ACM,1993,62-73.
[7] Canetti R, Goldreich O, and Halevi S. The random oracle methodology, revisited[J]. Journal of the ACM (JACM),2004,51(4):557-594.
[8] Canetti R and Krawczyk H. Analysis of key-exchange protocols and their use forbuilding secure channels [C]. In: Proceeding of the International Conference onthe Theory and Application of Cryptographic Techniques: Advances in Cryptology,London: Springer-Verlag,2001,453-474.
[9] Canetti R. Universally composable security: a new paradigm for cryptographicprotocols [C]. In: Proceeding of42ndIEEE Computer Society Symposium onFoundations of Computer Science. Washington DC: IEEE Computer Society,2001,136-145.
[10] Canetti R. Universally composable signature, certification, and authentication [C].In: Proceeding of the17thIEEE Workshop on Computer Security Foundations.Washington DC: IEEE Computer Society,2004,219-233.
[11]冯涛.通用可复合密码协议理论及其应用研究[D].西安:西安电子科技大学,2008.
[12]张帆.无线网络安全协议的形式化分析方法[D].西安:西安电子科技大学，2007.
[13]杨超.无线网络协议的形式化分析与设计[D].西安:西安电子科技大学，2007.
[14]曹春杰.可证明安全的认证及密钥交换协议设计与分析[D].西安:西安电子科技大学,2008.
[15]张俊伟.密码协议的可组合安全[D].西安:西安电子科技大学，2010.
[16]徐海霞.分布式密钥分发方案的安全性证明[J].软件学报,2005,16(004):570-576.
[17]雷飞宇. UC安全多方计算模型及其典型应用研究[D].上海:上海交通大学，2007.
[18] Yao A, Yao F, and Zhao Y. A note on the feasibility of generalized universalcomposability. Mathematical Structures in Computer Science [J],2009,19(01):193-205.
[19] Gong L, Needham R, and Yahalom R. Reasoning about belief in cryptographicprotocols [C]. In: Proceeding of1990IEEE Computer Society Symposium onResearch in Security and Privacy. Washington DC: IEEE Computer Society,1990,234-248.
[20] Abadi M and Tuttle M. A Semantics for a Logic of Authentication [C]. In:PODC’91Proceedings of the10thAnnual ACM Symposium on Principles ofDistributed Computing, New York: ACM,1991,201-216.
[21] Kailar R. Reasoning about accountability in protocols for electronic commerce [C].In: SP’95Proceedings of the1995IEEE Symposium on Security and Privacy,Washington DC: IEEE Computer Society,1995,236.
[22] Perrig A and Song D. Looking for diamonds in the desert-extending automaticprotocol generation to three-party authentication and key agreement protocols [C].In: Proceeding of the13thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,2000,64-76.
[23] Song D. Athena. a new efficient automatic checker for security protocol analysis[C]. In: Proceedings of the12thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,1999,192-202.
[24] Hoare C A R. Communicating Sequential Processes [J]. Communications of theACM,1978,21(8):666-677.
[25] Roscoe AW. Modeling and Verifying Key exchange Protocols Using CSP and FDR[C]. In: Proceedings of the8thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,1995,98-107.
[26] Lowe G. Breaking and Fixing the Needham-Schroeder Public-Key Protocol UsingFDR [J]. Software Concepts and Tools,1996,17(3):93-102.
[27] Schneider S. Sidiropoulos A. CSP and Anonymity [C]. In: ESORICS’96Proceedings of the4thEuropean Symposium on Research in Computer Security,London: Springer-Verlag,1996,198-218.
[28] Ryan P, Schneider S, Lowe G, Roscoe B. The Modeling and analysis of SecurityProtocols: the csp approach [M]. Addison-Wesley Professional,2000,320.
[29] Abadi M, Andrew D G. A calculus for cryptographic Protocols: The Spi calculus[J]. Information and Computation,1999,148(1):1-70.
[30] Abadi M, Fournet C. Mobile values, new names, and secure communication [C]. In:POPL’01Proceedings of the28thACM SIGPLAN-SIGACT symposium onPrinciples of programming languages, New York: ACM,2001,104-115.
[31] Datta A, Dereka A, Mitchell J. A derivation system and compositional logic forsecurity protocols [J]. Journal of Computer Security,2005,13(3):423-482.
[32] Harkins D, Carrel D. The internet key exchange (IKE)[EB/OL],1998.http://www.ietf.org/rfc/rfc2409.txt
[33] Diffie W, Orschot P, Eiener M. Authentication and authenticated key exchanges [J].Designs, Codes and Cryptography,1992,2(2):107-125.
[34] Bellovin S and Aiello W. Just Fast Keying (JFK)[EB/OL].2002.http://www.cs.columbia.edu/~angelos/Papers/draft-keromytis-jfk-04.txt
[35] Paulson L C. Mechanized proofs for a recursive authentication protocol [C]. In:CSFW’97Proceedings of the10thIEEE workshop on Computer SecurityFoundations, Washington DC: IEEE Computer Society,1997,84-95.
[36] Paulson L C. The inductive approach to verifying cryptographic protocols [J].Journal of Computer Security,1998,6(1-2):85-128.
[37] Durgin N, Mitchell J, Pavlovic D. A compositional logic for proving securityproperties of protocols [J]. Journal of Computer Security,2003,11(4):667-721.
[38] Datta A, Derek A, Mitchell J. A derivation system for security protocols and itslogical formalization [C]. In: Proceedings of16thIEEE Computer SecurityFoundations Workshop, Washington DC: IEEE Computer Society,2003,109-125.
[39] Datta A, Derek A, Mitchell J. Secure protocol composition [C]. In: Proceedings ofthe2003ACM workshop on Formal methods in Security engineering, New York:ACM,2003,11-23.
[40] Datta A, Derek A, Mitchell J. Abstraction and refinement in protocol derivation[C]. In: Proceedings of17thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,2004,30-45.
[41] Datta A, Derek A, Mitchell J. Probabilistic polynomial-time semantics for aprotocol security logic [C]. In: Proceedings of32ndInternational Colloquim onAutomata, Languages and Programming, Berlin Heidelberg: Springer-Verlag,2005,16-29.
[42] Datta A, Derek A, Mitchell J. Computationally sound compositional logic for keyexchange protocols [C]. In: CSFW’06Proceedings of19thIEEE workshop onComputer Security Foundations, Washington DC: IEEE Computer Society,2006,321-334.
[43] Datta A, Derek A, Mitchell J. Protocol composition logic (PCL). Electronic Notesin Theoretical Computer Science [J],2007,172:311-358.
[44] Roy A, Datta A, DereK A, et al. Secrecy analysis in protocol composition logic [C].ASIAN’06Proceedings of the11thAsian computing science conference onAdvances in Computer Science: Secure Software and Related Issues, BerlinHeidelberg: Springer-Verlag,2006,197-213.
[45] Datta A, Franklin J, Garg D. A logic of secure systems and its application totrusted computing. In: Proceedings of200930thIEEE Symposium on Security andPrivacy, Washington DC: IEEE Computer Society,2009,221-236.
[46] He C, Sundararajan M, Datta A, et al. A modular correctness proof of IEEE802.11iand TLS [C]. In: CCS’05Proceedings of the12thACM conference on Computerand Communications Security, New York: ACM,2005,2-15.
[47]冯涛,张子彬,马建峰.协议组合逻辑安全的WiMAX无线网络认证协议[J].电子与信息学报.2009,32(9):2016-2011.
[48]铁满霞,李建东,王育民.WAPI密钥管理协议的PCL证明[J].电子与信息学报.2009,31(2):444-447.
[49]刘锋,李舟军,李梦君.使用协议组合逻辑PCL验证AmendedNeedham-Schroeder协议[J],计算机工程与科学,2008,30(11):13-15.
[50]王惠斌,祝跃飞,常青美.协议组合逻辑系统研究[J],郑州大学学报(理学版),2008,40(4):56-59.
[51] Abadi M. Rogaway P. Reconciling two views of cryptography (the computationalsoundness of formal encryption)[J]. Journal of Cryptology,2002,15(2):103-127.
[52] Abadi M, Rogaway P: Reconciling two views cryptography (the computationalsoundness of formal encryption)[C]. In: TCS’00Proceedings of InternationalConference on Theoretical Computer Science, Exploring New Frontiers ofTheoretical Informatics, London: Springer-Verlag,2000,3-22.
[53] Veronique C, Steve K, Bogdan W. A survey of symbolic methods in computationalanalysis of cryptographic systems [J]. Journal of Automated Reasoning,2010,46:3-4.
[54] Dolev D, Yao A. on the security of public key protocols. IEEE Transaction onInformation Theory,1983,29(2):198-208.
[55] Micciancio D, Warinschi B. Completeness theorems for the Abadi-Rogaway logicof encrypted expressions [J], Journal of Computer Security,2004,12(1):99-129.
[56] Blanchet B. Computationally sound Mechanized Prover for security protocols [J].IEEE Transactions on Dependable and Secure Computing,2008,5(4):193-207.
[57] Cortier V, Kremer S, Kusters R, Warinschi B. Computationally sound symbolicsecrecy in the presence of hash functions [C]. In: Proceedings of the26thconference on Foundations of Software Technology and Theoretical ComputerScience, London: Springer-Verlag,2006,4337:176-187.
[58] Galindo D, Garcia F D, Van Rossum P. Computational soundness of non-malleablecommitments [C]. In: ISPEC’08Proceedings of the4thInternational conference onInformation Security Practice and Experience, Berlin Heidelberg: Springer-Verlag,2008,4991:361-376.
[59] Backes M, Unruh D. Computational soundness of symbolic zero-knowledge proofsagainst active attackers [C]. In: CSF’08Proceedings of the21stIEEE ComputerSecurity Foundations Symposium, Washington DC: IEEE Computer Society,2008,255-269.
[60] Delaune S, Kremer S, and Ryan M.D. Coercion-resistance and receipt-freeness inelectronic voting [C]. In: CSFW’06Proceedings of the19thIEEE workshop onComputer Security Foundations, Washington DC: IEEE Computer Society,2006,28-42.
[61] Backes M, Pfitzmann B, and Waidner M. The reactive simulatability (RSIM)framework for asynchronous systems [J]. Journal of Information and Computer,2007,205(12):1685-1720.
[62] Kusters R, Tuengerthal M. Joint state theorems for public-key encryption anddigital signature functionalities with local computations [C]. In: CSF’08Proceedings of the200821stIEEE Computer Security Foundations Symposium,Washington DC: IEEE Computer Society,2008,270-284.
[63] Milner R. A calculus of communication systems [M], Lecture Notes in ComputerScience, vol92, London: Springer-Verlag,1998.
[64] Comon-Lundh H, Cortier V. Computational soundness of observationalequivalence [C]. In: CCS’08Proceedings of the15thACM Conference onComputer and Communications Security, New York: ACM,2008,109-118.
[65] Canetti R, Herzog J. Universally composable symbolic security analysis [J].Journal of Cryptology,2011,42(1):83-147.
[66] Canetti R, Gajek S. Universally composable symbolic analysis of Diffie-Hellmanbased key exchange [EB/OL],2010. Http://eprint.iacr.org/iacr.org/2010/303.pdf.
[67] Datta A, Derek A, Mitchell J, Warinschi B. Computationally sound compositionallogic for key exchange [C]. In: Proceedings of19thIEEE Computer SecurityFoundations Workshop, Washington DC: IEEE Computer Society,2006,321-334.
[68] Roy A, Datta A, Derek A, Mitchell J.C. Inductive proofs of computational secrecy
[C]. In: ESORICS’07Proceedings of the12thEuropean Symposium on Research inComputer Security, Berlin Heidelberg: Springer-Verlag,2007,4734:219-234.
[69] Roy A, Datta A, Mithchell J.C. Formal proofs of cryptographic security ofDiffie-Hellman based protocols [C]. In: TGC’07Proceeding of the3rdConferenceon Trustworthy global computing, Berlin Heidelberg: Springer-Verlag,2008,4912:312-329.
[70] Gupta P, Shmatikov V. Towards computationally sound symbolic analysis of keyexchange protocols [C]. In: FMSE’05Proceedings of the2005ACM Workshop onFormal Methods in Security Engineering, New York: ACM,2005,23-32.
[71] Gupta P, Shmatikov V. Key confirmation and adaptive corruptions in the protocolsecurity logic [C]. In: FCS-ARSPA’06Proceedings Of the Joint Workshop onFoundations of Computer Security and Automated Reasoning for Security ProtocolAnalysis, Washington DC: IEEE Computer Society,2006,113-142.
[72]赵华伟.两种安全协议形式化理论的研究[D],山东:山东大学,2006.
[73]尹学永,调和两种观点的安全协议形式化分析方法研究[D],山东:山东大学,2009.
[74]罗正钦,基于UC框架的安全协议形式化分析[D],上海:上海交通大学,2008.
[75] Jean G L, Catuscia P, Angelo T. A probabilistic applied pi calculus [C]. In:APLAS’07Proceedings of the5thAsian Conference on Programming languagesand Systems, Berlin Heidelberg: Springer-Verlag,2007,175-190.
[76] Acs G, Buttyan L, Vajda I. Provably secure on-demand source routing in mobile adhoc networks [J]. IEEE Transactions on Mobile Computing,2006,5(11):1533-1546.
[77] Hu Y C, Perrig A, and Johnson D B. Ariadne: A Secure On-Demand RoutingProtocol for Ad Hoc Networks [J]. Wireless Networks,2005,11(2):12–23.
[78] Papdimitratos P, Haas Z. Secure routing for mobile ad hoc networks [C]. In:Proceedings of the communication Networks and Distributed Systems Modelingand Simulation, Washington DC: IEEE Computer Society,2002,27-31.
[79] Acs G, Buttyan L, Vajda I. Towards provable security for ad hoc routing protocols
[C]. In: ESAS’05Proceeding of2th European workshop on Security and privacyin Ad hoc and Sensor Networks, Berlin Heidelberg: Springer-Verlag,2005,3813:113-127.
[80] Burmester M, Medeiros B. On the Security of Discovery in MANETs [J]. IEEETransactions on Mobile Computing.2007,8(9):1180-1188.
[81]冯涛,郭显,马建峰,李兴华.可证明安全的节点不相交多路径源路由协议.软件学报[J],2010,21(7):1717-1731.
[82]郭显.无线Ad Hoc网络安全路由协议关键技术研究[D],兰州:兰州理工大学,2009.
[83]王英龙,王继志,王美琴.基于BAN逻辑的Ad Hoc移动网络路由协议的安全性分析[J].通信学报,2005,26(4):125-129.
[84] Ghazizadeh S, Ilghami o, Sirin E, and Yaman F. Security-aware adaptive dynamicsource routing protocol [C]. In: Proceedings of27thAnnual IEEE Conference onLocal Computer Networks, Washington DC: IEEE Computer Society,2002,751-760.
[85]刘晶,伏飞,肖军模.一种安全DSR协议的形式化分析方法[J].解放军理工大学学报(自然科学版),2009,10(4):423-429.
[86] Yang S H, Baras J S. Modeling vulnerabilities of ad hoc routing protocols [C]. In:Proceedings of the1stACM Workshop on Security of Ad hoc and Sensor Networks.New York: ACM,2003,12-20.
[87]王继志,王英龙.基于改进的串空间分析Ad Hoc路由协议安全性[J].软件学报,2006,17:256-261.
[88]董学文,马建峰,牛文生等.基于串空间的Ad Hoc安全路由协议攻击分析模型[J].软件学报,2011,22(7):1641-1651.
[89] Prasad K V S. A Calculus of Broadcasting Systems [J]. Science of ComputerProgramming,1995,25(2-3):285-327.
[90] Ene C, Muntean T. A Broadcast based Calculus for Communicating Systems [C].In: IPDPS’01Proceedings of the15thInternational Parallel&DistributedProcessing Symposium, Washington DC: IEEE Computer Society,2001,149.
[91] Nanz S, Hankin C. A Framework for Security Analysis of Mobile WirelessNetworks [J]. Theoretical Computer Science,2006,367(1-2):203-227.
[92] Singh A, Ramakrishnan C R, and Smolka S A. A Process Calculus for Mobile AdHoc Networks [C]. In: COORDINA’08Proceedings of the10thinternationalconference on Coordination models and languages, Berlin Heidelberg:Springer-Verlag,2008,296-314.
[93] Godskesen J C. A Calculus for Mobile Ad Hoc Networks [J]. Lecture Notes inComputer Science,2009,242(1):161-183.
[94] Sanzgir K, LaFlamme D, Dahil B, Neil Levine B. Authenticated routing for ad hocnetworks [J]. IEEE Journal on Selected Areas in Communication, Special Issue onWireless Ad Hoc Networks,2005,23(3):598-610.
[95]李沁,曾庆凯.利用类型推理验证Ad hoc安全路由协议[J].软件学报,2009,20(10):2822-2833.
[96] Goldwasser S, Micali S, Rackoff C. The knowledge complexity of interactiveproof-systems [J], SIAM Journal on Computing,1989,18(1):186-208.
[97] Nanz S. Specification and Security Analysis of Mobile Ad-Hoc networks [D],London: Imperial college,2006.
[98] Todd R A, Yasinsac A. Adaptive Threat Modeling for Secure Ad Hoc RoutingProtocols [J]. Electronic Notes in Theoretical Commputer Science (ENTCS),2008,197(2):3-14.
[99] Cordasco J, Wetzel S. An attacker model for MANET routing security [C]. In:WiSec’09Proceedings of the Second ACM Conference on Wireless NetworkSecurity, New York: ACM,2009,87-94.
[100] Brik V, Banerjee S, Gruteser M, Oh S. Wireless Device Identification withRadiometric Signatures [C]. In: MobiCom’08Proceeding of the14th ACMInternational Conference on Mobile Computing and Networking, New York:ACM,2008,116-127.
[101] Sanzgiri K, Dahill B, Levine B, Shields C. A secure routing protocol for ad hocnetworks [C]. In: ICNP’02Proceedings of the10th IEEE InternationalConference on Networks Protocols, Washington DC: IEEE Computer Society,2002,78-89.
[102] Johnson D, Maltz D, Hu Y-C. The Dynamic Source Routing Protocol for MobileAd Hoc Networks (DSR)[EB/OL].http://www.ietf.org/internet-drafts/draft-ietf-manet-dsr-10.txt,2005.
[103] Perkins C, Royer E. Ad hoc on-demand distance vector routing [J]. MobileSystems and Applications.1999,24(3):59-81.
[104] Changwen L, Mark Y, Wsteven C, Guo X G. Guaranteed On-Demand Discory ofNode-Disjoint Paths in Ad hoc Networks [J]. Computer communications,2007,30:2917-2930.
[105] Kotzanikolaou P, Mavropodi R, Douligeris C. Secure Multi-path Routing forMobile Ad hoc Networks [J]. Ad hoc networks,2007,5(1):87-99
[106] Lee S J, Gerla M. SMR: Split Multipath Routing with Maximally Disjoint Pathsin Ad hoc Networks [C]. In: ICC’01Proceedings of IEEE InternationalConference on Communications, Washington DC: IEEE Computer Society,2001,10:3201-3205.
[107] Berton S, Yin H, Lin C, Ge Y M. Secure, Disjoint, Multipath Source RoutingProtocol(SDMSR) for Mobile Ad-Hoc Networks [C]. In: GCC’06Proceedings ofthe Fifth International Conference on Grid and Cooperative Computing,Washington DC: IEEE Computer Society,2006,387-394.
[108] Ye Z, Krishnamurthy S V, Tripathi S K. A Framework for Reliable Routing inMobile Ad Hoc Net-works [C]. In: INFOCOM’03Proceedings of Twenty-SecondAnnual Joint Conference on the IEEE Computer and Communications Societies,Washington DC: IEEE Computer Society,2003,1:270-280.
[109] Abbas A M, Jain B N. Path Diminution is Unavoidable in Node-DisjointMultipath Routing in a Single Route Discovery [C]. In: COMSWARE’06Proceedings of1st IEEE International conference on Communication Softwareand Middleware, Washington DC: IEEE Computer Society,2006,1-10.
[110] Cormen T H, Leiserson C E, Rivest R L. Introduction to Algorithms [M]. SecondEdition, Cambridge, MA,The MIT Press,1993.
[111] Newsome J, Shi E, Song D, Perrig A. The sybil attack in sensor networks:analysis&defenses [C]. In: IPSN’04Proceedings of the3rd InternationalSymposium on Information Processing in Sensor Networks, New York: ACM,2004,259-268.
[112] Hu YC, Perrig A, Johnson D. Packet leashes: A defense against wormhole attacksin wireless ad hoc networks [C]. In: INFOCOM’03Proceedings of the22ndAnnual Joint Conference of the IEEE Computer and Communications Societies,Washington DC: IEEE Computer Society,2003,3:1976-1986.
[113]浦保兴,杨路明,王伟平.线性网络编码的导出与扩展[J].软件学报,2011,22(3):558-571.
[114]付彬,李仁发,刘彩苹,肖雄仁.无线传感器网络中一种基于网络编码的拥塞感知路由协议[J].计算机研究与发展,2011,48(6):991-999.
[115]卢翼,肖嵩,吴成柯.基于机会式网络编码的低时延广播传输算法[J],电子学报,2011,39(5):1214-1219.
[116]浦保兴,王伟平.线性网络编码运算代价的估算与分析[J].通信学报,2011,32(5):47-55.
[117]王蔚,喻莉,朱光喜,李挥.基于网络编码的感知无线网多中继机制[J].电子与信息学报,2011,33(4):869-873.
[118]焦贤龙,王晓东,周兴铭.采用启发是算法的无线自组网网络编码方法[J].软件学报,2010,21(11):2892-2905.
[119]陈贵海,李宏兴,韩松.多跳无线网络中基于网络编码的多路径路由[J],软件学报,2010,21(8):1908-1919.
[120]王晓东,霍广城,孙海燕.移动自组织网中基于部分网络编码的机会主义路由[J],电子学报,2010,38(8):1736-1740.
[121] Sengupta S, Rayanchu S, Banerjee S. Network Coding-Aware Routing inWireless Networks [J], IEEE/ACM Transactions on Networking,2010,18(4):1158-1170.
[122] Le J L, John C S, Lui D M C. DCAR: Dsitributed Coding-Aware Routing inWireless Networks [J], IEEE Transactions on Mobile Computing,2010,9(4):596-608.
[123] Katti S, Rahul H, Hu W. XORs in the Air:Practical Wireless Network Coding [J].IEEE/ACM Transactions on Networking,2008,16(3):497-510.
[124] Dong J, Curtmola R, Nita-Rotaru C. Secure Network Coding for Wireless MeshNetworks: Threats, Challenges, and Directions [J], Computer Communications,2009,32(17):1790-1801.
[125] Kannhavong B, Nakayama H, Nemoto Y, Kato N, Jamalipour A. A Survey ofRouting Attacks in Mobile Ad Hoc Networks [J], Wireless Communication,2007,14(5):85-91.
[126] Peng S C, Jia W J, Wang G J. Trusted Routing Based on Dynamic TrustMechanism in Mobile Ad Hoc Networks [J], IEICE Transactions on Informationand Systems,2010, E93.D(3):510-517.
[127] Ghosh T, Pissinou N, Makki K. Towards Designing a Trusted Routing Solution InMobile Ad Hoc Networks [J], Mobile Networks and Applications,2005,10(6):985-995.
[128] Canetti R. A unified framework for analyzing cryptographic protocols [R], ECCCTR01-16. http://eprint.iacr.org/2000/067.
[129] Küsters R, Tuengerthal M. Universally Composable Symmetric Encryption [C].In: CSF’09Proceedings of the200922nd IEEE Computer Security FoundationsSymposium, Washington DC: IEEE Computer Society,2009,293-307.
[2] Fabrega F, Herzog J, and Gurrman J. Strand Spaces: Proving security protocolscorrect [J]. Journal of Computer Security,1999,7(2):191-230.
[3] Backes M, Pfitzmann B, and Waidner M. The reactive simulatability framework [J].Information and Computation,2007,205(12):1685-1720.
[4] Hu Y. C, Perrig A. A survey of secure wireless ad hoc routing [J]. IEEE Security&Privacy,2004,2(3):28-39.
[5] TODD R, Yasinsac A. Surveying Security Analysis Techniques in MANETRouting Protocols [J], IEEE Communications,2007,9(4):69-84.
[6] Bellare M and Rogaway P. Random Oracles are practical: A paradigm fordesigning efficient protocols [C]. In: Proceeding of the1stACM conference onComputer and Communications Security. New York: ACM,1993,62-73.
[7] Canetti R, Goldreich O, and Halevi S. The random oracle methodology, revisited[J]. Journal of the ACM (JACM),2004,51(4):557-594.
[8] Canetti R and Krawczyk H. Analysis of key-exchange protocols and their use forbuilding secure channels [C]. In: Proceeding of the International Conference onthe Theory and Application of Cryptographic Techniques: Advances in Cryptology,London: Springer-Verlag,2001,453-474.
[9] Canetti R. Universally composable security: a new paradigm for cryptographicprotocols [C]. In: Proceeding of42ndIEEE Computer Society Symposium onFoundations of Computer Science. Washington DC: IEEE Computer Society,2001,136-145.
[10] Canetti R. Universally composable signature, certification, and authentication [C].In: Proceeding of the17thIEEE Workshop on Computer Security Foundations.Washington DC: IEEE Computer Society,2004,219-233.
[11]冯涛.通用可复合密码协议理论及其应用研究[D].西安:西安电子科技大学,2008.
[12]张帆.无线网络安全协议的形式化分析方法[D].西安:西安电子科技大学，2007.
[13]杨超.无线网络协议的形式化分析与设计[D].西安:西安电子科技大学，2007.
[14]曹春杰.可证明安全的认证及密钥交换协议设计与分析[D].西安:西安电子科技大学,2008.
[15]张俊伟.密码协议的可组合安全[D].西安:西安电子科技大学，2010.
[16]徐海霞.分布式密钥分发方案的安全性证明[J].软件学报,2005,16(004):570-576.
[17]雷飞宇. UC安全多方计算模型及其典型应用研究[D].上海:上海交通大学，2007.
[18] Yao A, Yao F, and Zhao Y. A note on the feasibility of generalized universalcomposability. Mathematical Structures in Computer Science [J],2009,19(01):193-205.
[19] Gong L, Needham R, and Yahalom R. Reasoning about belief in cryptographicprotocols [C]. In: Proceeding of1990IEEE Computer Society Symposium onResearch in Security and Privacy. Washington DC: IEEE Computer Society,1990,234-248.
[20] Abadi M and Tuttle M. A Semantics for a Logic of Authentication [C]. In:PODC’91Proceedings of the10thAnnual ACM Symposium on Principles ofDistributed Computing, New York: ACM,1991,201-216.
[21] Kailar R. Reasoning about accountability in protocols for electronic commerce [C].In: SP’95Proceedings of the1995IEEE Symposium on Security and Privacy,Washington DC: IEEE Computer Society,1995,236.
[22] Perrig A and Song D. Looking for diamonds in the desert-extending automaticprotocol generation to three-party authentication and key agreement protocols [C].In: Proceeding of the13thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,2000,64-76.
[23] Song D. Athena. a new efficient automatic checker for security protocol analysis[C]. In: Proceedings of the12thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,1999,192-202.
[24] Hoare C A R. Communicating Sequential Processes [J]. Communications of theACM,1978,21(8):666-677.
[25] Roscoe AW. Modeling and Verifying Key exchange Protocols Using CSP and FDR[C]. In: Proceedings of the8thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,1995,98-107.
[26] Lowe G. Breaking and Fixing the Needham-Schroeder Public-Key Protocol UsingFDR [J]. Software Concepts and Tools,1996,17(3):93-102.
[27] Schneider S. Sidiropoulos A. CSP and Anonymity [C]. In: ESORICS’96Proceedings of the4thEuropean Symposium on Research in Computer Security,London: Springer-Verlag,1996,198-218.
[28] Ryan P, Schneider S, Lowe G, Roscoe B. The Modeling and analysis of SecurityProtocols: the csp approach [M]. Addison-Wesley Professional,2000,320.
[29] Abadi M, Andrew D G. A calculus for cryptographic Protocols: The Spi calculus[J]. Information and Computation,1999,148(1):1-70.
[30] Abadi M, Fournet C. Mobile values, new names, and secure communication [C]. In:POPL’01Proceedings of the28thACM SIGPLAN-SIGACT symposium onPrinciples of programming languages, New York: ACM,2001,104-115.
[31] Datta A, Dereka A, Mitchell J. A derivation system and compositional logic forsecurity protocols [J]. Journal of Computer Security,2005,13(3):423-482.
[32] Harkins D, Carrel D. The internet key exchange (IKE)[EB/OL],1998.http://www.ietf.org/rfc/rfc2409.txt
[33] Diffie W, Orschot P, Eiener M. Authentication and authenticated key exchanges [J].Designs, Codes and Cryptography,1992,2(2):107-125.
[34] Bellovin S and Aiello W. Just Fast Keying (JFK)[EB/OL].2002.http://www.cs.columbia.edu/~angelos/Papers/draft-keromytis-jfk-04.txt
[35] Paulson L C. Mechanized proofs for a recursive authentication protocol [C]. In:CSFW’97Proceedings of the10thIEEE workshop on Computer SecurityFoundations, Washington DC: IEEE Computer Society,1997,84-95.
[36] Paulson L C. The inductive approach to verifying cryptographic protocols [J].Journal of Computer Security,1998,6(1-2):85-128.
[37] Durgin N, Mitchell J, Pavlovic D. A compositional logic for proving securityproperties of protocols [J]. Journal of Computer Security,2003,11(4):667-721.
[38] Datta A, Derek A, Mitchell J. A derivation system for security protocols and itslogical formalization [C]. In: Proceedings of16thIEEE Computer SecurityFoundations Workshop, Washington DC: IEEE Computer Society,2003,109-125.
[39] Datta A, Derek A, Mitchell J. Secure protocol composition [C]. In: Proceedings ofthe2003ACM workshop on Formal methods in Security engineering, New York:ACM,2003,11-23.
[40] Datta A, Derek A, Mitchell J. Abstraction and refinement in protocol derivation[C]. In: Proceedings of17thIEEE Computer Security Foundations Workshop,Washington DC: IEEE Computer Society,2004,30-45.
[41] Datta A, Derek A, Mitchell J. Probabilistic polynomial-time semantics for aprotocol security logic [C]. In: Proceedings of32ndInternational Colloquim onAutomata, Languages and Programming, Berlin Heidelberg: Springer-Verlag,2005,16-29.
[42] Datta A, Derek A, Mitchell J. Computationally sound compositional logic for keyexchange protocols [C]. In: CSFW’06Proceedings of19thIEEE workshop onComputer Security Foundations, Washington DC: IEEE Computer Society,2006,321-334.
[43] Datta A, Derek A, Mitchell J. Protocol composition logic (PCL). Electronic Notesin Theoretical Computer Science [J],2007,172:311-358.
[44] Roy A, Datta A, DereK A, et al. Secrecy analysis in protocol composition logic [C].ASIAN’06Proceedings of the11thAsian computing science conference onAdvances in Computer Science: Secure Software and Related Issues, BerlinHeidelberg: Springer-Verlag,2006,197-213.
[45] Datta A, Franklin J, Garg D. A logic of secure systems and its application totrusted computing. In: Proceedings of200930thIEEE Symposium on Security andPrivacy, Washington DC: IEEE Computer Society,2009,221-236.
[46] He C, Sundararajan M, Datta A, et al. A modular correctness proof of IEEE802.11iand TLS [C]. In: CCS’05Proceedings of the12thACM conference on Computerand Communications Security, New York: ACM,2005,2-15.
[47]冯涛,张子彬,马建峰.协议组合逻辑安全的WiMAX无线网络认证协议[J].电子与信息学报.2009,32(9):2016-2011.
[48]铁满霞,李建东,王育民.WAPI密钥管理协议的PCL证明[J].电子与信息学报.2009,31(2):444-447.
[49]刘锋,李舟军,李梦君.使用协议组合逻辑PCL验证AmendedNeedham-Schroeder协议[J],计算机工程与科学,2008,30(11):13-15.
[50]王惠斌,祝跃飞,常青美.协议组合逻辑系统研究[J],郑州大学学报(理学版),2008,40(4):56-59.
[51] Abadi M. Rogaway P. Reconciling two views of cryptography (the computationalsoundness of formal encryption)[J]. Journal of Cryptology,2002,15(2):103-127.
[52] Abadi M, Rogaway P: Reconciling two views cryptography (the computationalsoundness of formal encryption)[C]. In: TCS’00Proceedings of InternationalConference on Theoretical Computer Science, Exploring New Frontiers ofTheoretical Informatics, London: Springer-Verlag,2000,3-22.
[53] Veronique C, Steve K, Bogdan W. A survey of symbolic methods in computationalanalysis of cryptographic systems [J]. Journal of Automated Reasoning,2010,46:3-4.
[54] Dolev D, Yao A. on the security of public key protocols. IEEE Transaction onInformation Theory,1983,29(2):198-208.
[55] Micciancio D, Warinschi B. Completeness theorems for the Abadi-Rogaway logicof encrypted expressions [J], Journal of Computer Security,2004,12(1):99-129.
[56] Blanchet B. Computationally sound Mechanized Prover for security protocols [J].IEEE Transactions on Dependable and Secure Computing,2008,5(4):193-207.
[57] Cortier V, Kremer S, Kusters R, Warinschi B. Computationally sound symbolicsecrecy in the presence of hash functions [C]. In: Proceedings of the26thconference on Foundations of Software Technology and Theoretical ComputerScience, London: Springer-Verlag,2006,4337:176-187.
[58] Galindo D, Garcia F D, Van Rossum P. Computational soundness of non-malleablecommitments [C]. In: ISPEC’08Proceedings of the4thInternational conference onInformation Security Practice and Experience, Berlin Heidelberg: Springer-Verlag,2008,4991:361-376.
[59] Backes M, Unruh D. Computational soundness of symbolic zero-knowledge proofsagainst active attackers [C]. In: CSF’08Proceedings of the21stIEEE ComputerSecurity Foundations Symposium, Washington DC: IEEE Computer Society,2008,255-269.
[60] Delaune S, Kremer S, and Ryan M.D. Coercion-resistance and receipt-freeness inelectronic voting [C]. In: CSFW’06Proceedings of the19thIEEE workshop onComputer Security Foundations, Washington DC: IEEE Computer Society,2006,28-42.
[61] Backes M, Pfitzmann B, and Waidner M. The reactive simulatability (RSIM)framework for asynchronous systems [J]. Journal of Information and Computer,2007,205(12):1685-1720.
[62] Kusters R, Tuengerthal M. Joint state theorems for public-key encryption anddigital signature functionalities with local computations [C]. In: CSF’08Proceedings of the200821stIEEE Computer Security Foundations Symposium,Washington DC: IEEE Computer Society,2008,270-284.
[63] Milner R. A calculus of communication systems [M], Lecture Notes in ComputerScience, vol92, London: Springer-Verlag,1998.
[64] Comon-Lundh H, Cortier V. Computational soundness of observationalequivalence [C]. In: CCS’08Proceedings of the15thACM Conference onComputer and Communications Security, New York: ACM,2008,109-118.
[65] Canetti R, Herzog J. Universally composable symbolic security analysis [J].Journal of Cryptology,2011,42(1):83-147.
[66] Canetti R, Gajek S. Universally composable symbolic analysis of Diffie-Hellmanbased key exchange [EB/OL],2010. Http://eprint.iacr.org/iacr.org/2010/303.pdf.
[67] Datta A, Derek A, Mitchell J, Warinschi B. Computationally sound compositionallogic for key exchange [C]. In: Proceedings of19thIEEE Computer SecurityFoundations Workshop, Washington DC: IEEE Computer Society,2006,321-334.
[68] Roy A, Datta A, Derek A, Mitchell J.C. Inductive proofs of computational secrecy
[C]. In: ESORICS’07Proceedings of the12thEuropean Symposium on Research inComputer Security, Berlin Heidelberg: Springer-Verlag,2007,4734:219-234.
[69] Roy A, Datta A, Mithchell J.C. Formal proofs of cryptographic security ofDiffie-Hellman based protocols [C]. In: TGC’07Proceeding of the3rdConferenceon Trustworthy global computing, Berlin Heidelberg: Springer-Verlag,2008,4912:312-329.
[70] Gupta P, Shmatikov V. Towards computationally sound symbolic analysis of keyexchange protocols [C]. In: FMSE’05Proceedings of the2005ACM Workshop onFormal Methods in Security Engineering, New York: ACM,2005,23-32.
[71] Gupta P, Shmatikov V. Key confirmation and adaptive corruptions in the protocolsecurity logic [C]. In: FCS-ARSPA’06Proceedings Of the Joint Workshop onFoundations of Computer Security and Automated Reasoning for Security ProtocolAnalysis, Washington DC: IEEE Computer Society,2006,113-142.
[72]赵华伟.两种安全协议形式化理论的研究[D],山东:山东大学,2006.
[73]尹学永,调和两种观点的安全协议形式化分析方法研究[D],山东:山东大学,2009.
[74]罗正钦,基于UC框架的安全协议形式化分析[D],上海:上海交通大学,2008.
[75] Jean G L, Catuscia P, Angelo T. A probabilistic applied pi calculus [C]. In:APLAS’07Proceedings of the5thAsian Conference on Programming languagesand Systems, Berlin Heidelberg: Springer-Verlag,2007,175-190.
[76] Acs G, Buttyan L, Vajda I. Provably secure on-demand source routing in mobile adhoc networks [J]. IEEE Transactions on Mobile Computing,2006,5(11):1533-1546.
[77] Hu Y C, Perrig A, and Johnson D B. Ariadne: A Secure On-Demand RoutingProtocol for Ad Hoc Networks [J]. Wireless Networks,2005,11(2):12–23.
[78] Papdimitratos P, Haas Z. Secure routing for mobile ad hoc networks [C]. In:Proceedings of the communication Networks and Distributed Systems Modelingand Simulation, Washington DC: IEEE Computer Society,2002,27-31.
[79] Acs G, Buttyan L, Vajda I. Towards provable security for ad hoc routing protocols
[C]. In: ESAS’05Proceeding of2th European workshop on Security and privacyin Ad hoc and Sensor Networks, Berlin Heidelberg: Springer-Verlag,2005,3813:113-127.
[80] Burmester M, Medeiros B. On the Security of Discovery in MANETs [J]. IEEETransactions on Mobile Computing.2007,8(9):1180-1188.
[81]冯涛,郭显,马建峰,李兴华.可证明安全的节点不相交多路径源路由协议.软件学报[J],2010,21(7):1717-1731.
[82]郭显.无线Ad Hoc网络安全路由协议关键技术研究[D],兰州:兰州理工大学,2009.
[83]王英龙,王继志,王美琴.基于BAN逻辑的Ad Hoc移动网络路由协议的安全性分析[J].通信学报,2005,26(4):125-129.
[84] Ghazizadeh S, Ilghami o, Sirin E, and Yaman F. Security-aware adaptive dynamicsource routing protocol [C]. In: Proceedings of27thAnnual IEEE Conference onLocal Computer Networks, Washington DC: IEEE Computer Society,2002,751-760.
[85]刘晶,伏飞,肖军模.一种安全DSR协议的形式化分析方法[J].解放军理工大学学报(自然科学版),2009,10(4):423-429.
[86] Yang S H, Baras J S. Modeling vulnerabilities of ad hoc routing protocols [C]. In:Proceedings of the1stACM Workshop on Security of Ad hoc and Sensor Networks.New York: ACM,2003,12-20.
[87]王继志,王英龙.基于改进的串空间分析Ad Hoc路由协议安全性[J].软件学报,2006,17:256-261.
[88]董学文,马建峰,牛文生等.基于串空间的Ad Hoc安全路由协议攻击分析模型[J].软件学报,2011,22(7):1641-1651.
[89] Prasad K V S. A Calculus of Broadcasting Systems [J]. Science of ComputerProgramming,1995,25(2-3):285-327.
[90] Ene C, Muntean T. A Broadcast based Calculus for Communicating Systems [C].In: IPDPS’01Proceedings of the15thInternational Parallel&DistributedProcessing Symposium, Washington DC: IEEE Computer Society,2001,149.
[91] Nanz S, Hankin C. A Framework for Security Analysis of Mobile WirelessNetworks [J]. Theoretical Computer Science,2006,367(1-2):203-227.
[92] Singh A, Ramakrishnan C R, and Smolka S A. A Process Calculus for Mobile AdHoc Networks [C]. In: COORDINA’08Proceedings of the10thinternationalconference on Coordination models and languages, Berlin Heidelberg:Springer-Verlag,2008,296-314.
[93] Godskesen J C. A Calculus for Mobile Ad Hoc Networks [J]. Lecture Notes inComputer Science,2009,242(1):161-183.
[94] Sanzgir K, LaFlamme D, Dahil B, Neil Levine B. Authenticated routing for ad hocnetworks [J]. IEEE Journal on Selected Areas in Communication, Special Issue onWireless Ad Hoc Networks,2005,23(3):598-610.
[95]李沁,曾庆凯.利用类型推理验证Ad hoc安全路由协议[J].软件学报,2009,20(10):2822-2833.
[96] Goldwasser S, Micali S, Rackoff C. The knowledge complexity of interactiveproof-systems [J], SIAM Journal on Computing,1989,18(1):186-208.
[97] Nanz S. Specification and Security Analysis of Mobile Ad-Hoc networks [D],London: Imperial college,2006.
[98] Todd R A, Yasinsac A. Adaptive Threat Modeling for Secure Ad Hoc RoutingProtocols [J]. Electronic Notes in Theoretical Commputer Science (ENTCS),2008,197(2):3-14.
[99] Cordasco J, Wetzel S. An attacker model for MANET routing security [C]. In:WiSec’09Proceedings of the Second ACM Conference on Wireless NetworkSecurity, New York: ACM,2009,87-94.
[100] Brik V, Banerjee S, Gruteser M, Oh S. Wireless Device Identification withRadiometric Signatures [C]. In: MobiCom’08Proceeding of the14th ACMInternational Conference on Mobile Computing and Networking, New York:ACM,2008,116-127.
[101] Sanzgiri K, Dahill B, Levine B, Shields C. A secure routing protocol for ad hocnetworks [C]. In: ICNP’02Proceedings of the10th IEEE InternationalConference on Networks Protocols, Washington DC: IEEE Computer Society,2002,78-89.
[102] Johnson D, Maltz D, Hu Y-C. The Dynamic Source Routing Protocol for MobileAd Hoc Networks (DSR)[EB/OL].http://www.ietf.org/internet-drafts/draft-ietf-manet-dsr-10.txt,2005.
[103] Perkins C, Royer E. Ad hoc on-demand distance vector routing [J]. MobileSystems and Applications.1999,24(3):59-81.
[104] Changwen L, Mark Y, Wsteven C, Guo X G. Guaranteed On-Demand Discory ofNode-Disjoint Paths in Ad hoc Networks [J]. Computer communications,2007,30:2917-2930.
[105] Kotzanikolaou P, Mavropodi R, Douligeris C. Secure Multi-path Routing forMobile Ad hoc Networks [J]. Ad hoc networks,2007,5(1):87-99
[106] Lee S J, Gerla M. SMR: Split Multipath Routing with Maximally Disjoint Pathsin Ad hoc Networks [C]. In: ICC’01Proceedings of IEEE InternationalConference on Communications, Washington DC: IEEE Computer Society,2001,10:3201-3205.
[107] Berton S, Yin H, Lin C, Ge Y M. Secure, Disjoint, Multipath Source RoutingProtocol(SDMSR) for Mobile Ad-Hoc Networks [C]. In: GCC’06Proceedings ofthe Fifth International Conference on Grid and Cooperative Computing,Washington DC: IEEE Computer Society,2006,387-394.
[108] Ye Z, Krishnamurthy S V, Tripathi S K. A Framework for Reliable Routing inMobile Ad Hoc Net-works [C]. In: INFOCOM’03Proceedings of Twenty-SecondAnnual Joint Conference on the IEEE Computer and Communications Societies,Washington DC: IEEE Computer Society,2003,1:270-280.
[109] Abbas A M, Jain B N. Path Diminution is Unavoidable in Node-DisjointMultipath Routing in a Single Route Discovery [C]. In: COMSWARE’06Proceedings of1st IEEE International conference on Communication Softwareand Middleware, Washington DC: IEEE Computer Society,2006,1-10.
[110] Cormen T H, Leiserson C E, Rivest R L. Introduction to Algorithms [M]. SecondEdition, Cambridge, MA,The MIT Press,1993.
[111] Newsome J, Shi E, Song D, Perrig A. The sybil attack in sensor networks:analysis&defenses [C]. In: IPSN’04Proceedings of the3rd InternationalSymposium on Information Processing in Sensor Networks, New York: ACM,2004,259-268.
[112] Hu YC, Perrig A, Johnson D. Packet leashes: A defense against wormhole attacksin wireless ad hoc networks [C]. In: INFOCOM’03Proceedings of the22ndAnnual Joint Conference of the IEEE Computer and Communications Societies,Washington DC: IEEE Computer Society,2003,3:1976-1986.
[113]浦保兴,杨路明,王伟平.线性网络编码的导出与扩展[J].软件学报,2011,22(3):558-571.
[114]付彬,李仁发,刘彩苹,肖雄仁.无线传感器网络中一种基于网络编码的拥塞感知路由协议[J].计算机研究与发展,2011,48(6):991-999.
[115]卢翼,肖嵩,吴成柯.基于机会式网络编码的低时延广播传输算法[J],电子学报,2011,39(5):1214-1219.
[116]浦保兴,王伟平.线性网络编码运算代价的估算与分析[J].通信学报,2011,32(5):47-55.
[117]王蔚,喻莉,朱光喜,李挥.基于网络编码的感知无线网多中继机制[J].电子与信息学报,2011,33(4):869-873.
[118]焦贤龙,王晓东,周兴铭.采用启发是算法的无线自组网网络编码方法[J].软件学报,2010,21(11):2892-2905.
[119]陈贵海,李宏兴,韩松.多跳无线网络中基于网络编码的多路径路由[J],软件学报,2010,21(8):1908-1919.
[120]王晓东,霍广城,孙海燕.移动自组织网中基于部分网络编码的机会主义路由[J],电子学报,2010,38(8):1736-1740.
[121] Sengupta S, Rayanchu S, Banerjee S. Network Coding-Aware Routing inWireless Networks [J], IEEE/ACM Transactions on Networking,2010,18(4):1158-1170.
[122] Le J L, John C S, Lui D M C. DCAR: Dsitributed Coding-Aware Routing inWireless Networks [J], IEEE Transactions on Mobile Computing,2010,9(4):596-608.
[123] Katti S, Rahul H, Hu W. XORs in the Air:Practical Wireless Network Coding [J].IEEE/ACM Transactions on Networking,2008,16(3):497-510.
[124] Dong J, Curtmola R, Nita-Rotaru C. Secure Network Coding for Wireless MeshNetworks: Threats, Challenges, and Directions [J], Computer Communications,2009,32(17):1790-1801.
[125] Kannhavong B, Nakayama H, Nemoto Y, Kato N, Jamalipour A. A Survey ofRouting Attacks in Mobile Ad Hoc Networks [J], Wireless Communication,2007,14(5):85-91.
[126] Peng S C, Jia W J, Wang G J. Trusted Routing Based on Dynamic TrustMechanism in Mobile Ad Hoc Networks [J], IEICE Transactions on Informationand Systems,2010, E93.D(3):510-517.
[127] Ghosh T, Pissinou N, Makki K. Towards Designing a Trusted Routing Solution InMobile Ad Hoc Networks [J], Mobile Networks and Applications,2005,10(6):985-995.
[128] Canetti R. A unified framework for analyzing cryptographic protocols [R], ECCCTR01-16. http://eprint.iacr.org/2000/067.
[129] Küsters R, Tuengerthal M. Universally Composable Symmetric Encryption [C].In: CSF’09Proceedings of the200922nd IEEE Computer Security FoundationsSymposium, Washington DC: IEEE Computer Society,2009,293-307.