网络可以使人们在任意地点和任意时间、以任意方式访问共享网络资源,同时随着网络的迅猛发展和应用领域的不断扩大,网络面临着越来越多的安全威胁,为了保证网络的安全运行和资源的有效利用,作为网络安全服务基础的安全协议越来越受到重视,但由于安全协议本身的复杂性、相关理论和工程技术的不成熟以及人们认识能力的局限性,使得在现有安全协议中不可避免地存在着安全缺陷。为了设计出更可靠的安全协议,形式化方法成为描述、设计和分析安全协议的有效工具,并得到相当深入的研究、并获到比较广泛和成功的运用。目前,在无线局域网的安全协议中不同程度地存在着安全缺陷,其中在802.11中的安全机制存在着致命的安全漏洞。近几年来,为了基于可信平台特性建立未来具有高安全性的计算机系统,可信计算组提出了在计算机的硬件平台上引入安全芯片架构和通过提供硬件的安全特性来提高系统安全性的安全体系结构。本论文深入研究了安全协议面向主体的形式描述、设计和分析,并运用本论文中提出的安全协议面向主体的形式描述、设计和分析方法,分别研究了无线局域网中WAPI的认证和密钥协商协议以及可信计算中的OIAP协议。本论文的贡献表现在:(1)在安全协议面向主体的逻辑描述语言的研究中,将主体遵从安全协议相互通信的过程看成主体通过通信行为传递拥有、知识和信念以及主体的拥有、知识和信念随时序单调增加的过程;基于拥有、知识、信念、发送、接收和时序建立了描述安全协议的形式语言;给出它的Kripke语义模型和真值语义解释;在安全协议元素的形式化描述中,运用面向主体的方法描述了参与安全协议运行的主体的特性及其角色,比较清晰、准确和全面地描述了安全协议中消息的可辨认性和新鲜性、密钥的特性以及认证与密钥分发的目的,根据提供的不同安全服务,将安全协议中的密码机制抽象为不同信道;运用该形式语言以面向主体的方法对Needham-Schroeder对称密钥协议进行了形式化描述;将该语言与CKT5对安全协议逻辑描述的表达能力进行了比较。(2)在安全协议面向主体的设计逻辑的研究中,创建了基于面向主体以及知识和信念逻辑的安全协议设计逻辑,给出了关于知识和信念、安全主体、权威主体、发送、接收、拥有、消息的可辨认性、消息的新鲜性、消息源和主体身份认证、密钥验证和密钥协商的公理,给出了三段论推理规则;根据提供的不同安全服务,将安全协议中的密码机制抽象为不同信道,形式化地描述了细化规则、合成规则、转发规则、规范消息规则、关联规则、全信息规则和优化消息规则7个安全协议设计规则;将安全协议的设计分为安全协议目的的确定、分析主体的角色及其特性、密码机制的确定、安全协议目的的细化、分析安全协议设计的初始假设、运用规范消息、关联和全信息规则设计单个消息、根据优化消息优化安全协议7个步骤;根据给出的设计逻辑、设计规则和设计步骤形式