密码协议是为了获得某种特定的安全目标而执行的一个两方或者多方分布算法,这个算法是一个确定的动作序列,动作序列发送和接收的关键消息是基于某些密码学操作而构造的,例如加密、签名、散列函数等。一直以来,研究者更多地专注于使用形式化方法对现有的密码协议进行分析与验证,更为审慎和成熟的研究思路是设计和建立专用的方法和执行工具,用以指导安全协议的初始设计。在协议设计的过程中,密码协议的可复合性是一个重要属性。当对某个密码学任务进行协议化设计时,我们希望能够将一个任务分解成几个子任务,子任务通常相对简单,最后使用复合技术将已经设计的子任务作为安全子程序复合为给定的密码学任务。在任意协议并行的情况下,通用可复合(Universally Composable,UC)安全模型实现了密码协议的可复合安全性,本文基于UC安全模型主要研究了以下三个内容:第一,基于UC安全模型的身份相交复合操作理论的研究。UC安全模型主要包括密码协议的UC安全定义和相关的复合操作理论。在参与方唯一身份的假设下,现有的复合操作方法和理论包括子程序替换通用复合操作和多实例相交状态通用复合操作两类。基于协议仿真安全定义,首次提出了协议参与方实体多身份相交情况的复合操作方法和理论。针对参与方实体新身份与旧身份同时出现在单一的协议实例中,身份相交复合操作理论试图说明在一个协议实例中参与方实体安全的实现多身份鉴别自证明问题,身份相交复合操作理论解决了某些实际应用需求的可证明安全问题,例如组播密钥管理GDOI协议。第二路由协议UC安全模型的研究。路由协议是一类特殊的密码协议,可证明安全的路由协议设计和分析一直是网络安全领域的开放问题。本文将UC安全模型引入路由协议可证明安全的研究,对该领域新的概念、技术和方法进行了有益的探索,首次提出了路由协议的UC安全模型。提出了节点不相交多路径源路由协议的形式化安全定义,设计和实现了可证明安全的多路径路由协议。第三,基于UC安全模型的应用研究。根据UC安全模型对密码协议设计和分析的三步方法论,即密码协议的UC安全定义、基于计算复杂性的困难问题假设、基于“理想函数”的协议实现和“协议仿真”的可证明安全分析,本文应用研究的内容除了组播密钥管理协议和多路径路由协议,主要包括两类情况,一方面针对构造安全多方计算协议的两个基础工具(不经意传输,可否认认证),基于新的复杂性理论安全原语,设计和实现了高效可证明安全的不经意传输协议和可否认认证协议,另一方面针对特殊的无线网络(例如,无线传感器网络,移动卫星通信网络)安全需求,设计和实现了可证明安全的密钥分配和建立协议。