移动自组网是一种新型的无线移动网络,也是一个新型的移动计算平台,它是由一组带有无线收发器的移动终端所组成的一个无基站多跳步临时性自治网络系统。主要应用在军事战场、抗洪救火、无法布线等特殊和紧急环境下,并具有固定计算平台所没有的一些特点,如平台的自组性,拓扑的动态性,结点的平等性,带宽的有限性,控制的分布性,安全的不可靠性等等。随着网络,特别是移动自组网对安全性和可靠性的依赖不断增强,催生出了一个新的研究领域——可信计算。可信计算技术被认为是从根本上解决安全问题的革命性技术,其核心是使用一个称之为信任平台模块(TPM)的安全芯片,将其作为信任根植入到各种平台的计算机中,创建安全体系结构,为应用程序提供安全的计算环境。目前,国内外在可信计算研究方面已经取得了初步的成果,但在移动自组网中对可信协议的设计、可信软件的建模的研究才刚刚起步。具有代表性的是移动自组网的安全路由协议,由于移动自组网的开放性和移动平台的非可信性,一直无法避免相关的恶意攻击,比如隧道攻击、自私结点攻击、顶点割攻击等。所以,需要采用一种新的策略和方法来保证移动自组织网路由的安全可信性。由此,本文对移动自组网下的可信路由协议及其可信软件的形式化建模技术进行研究:首先,提出了一种移动自组网下的可信路由协议DAAODV。该协议使用可信计算技术对移动结点的路由软件进行完整性保护,以约束路由结点的行为,使用直接匿名认证(DAA)和基于属性的远程认证(PBA)向远程结点证明自身平台的可信,以解决以往安全路由协议所不能避免的相关攻击;该协议基于DAA,不需使用可信第三方来进行结点之间的认证,以避免可信第三方带来的效率瓶颈问题;同时,该协议使用假名来标识结点的身份,并且DAA和PBA认证也具有匿名的性质,所以该协议是匿名的,可以避免流量分析等攻击;该协议中还提出了一种轻量级的签名认证算法,并用于假名的认证,以缓解DAA和PBA签名和认证的高运算负担,从而避免因此带来的DoS攻击。然后,基于前一步工作,提出了一种移动可信软件的形式化构造方法。通过该方法可以完成软件的规约设计、精化以及最终的实现设计,以保证移动通信协议在软件层次的可信。其中,提出一种移动可信软件的形式化规约TCSpec,TCSpec提供了一套可供安全调用接口,并能满足可信移动软件多方面功能的需求,然后,以移动可信路由软件DAAODV为案例,给出调用TCSpec并完成移动软件设计的方法,最后,通过证明,得出结论:通过TCSpec形式化规约对移动软件进行设计,可保证其私有信息不泄露给非可信的结点。最后,对DAAODV协议进一步改进,提出了基于模糊集合理论的可信路由协议FuzzyAODV。该协议同样基于可信计算技术,并使用了DAA和PBA协议进行结点间的认证,但对DAAODV的认证消息格式重新定义,并对认证过程进行简化,提高了可信路由协议的运行效率;另外,FuzzyAODV额外考虑了恶意结点对路由过程的效率影响,首先分析该协议面临的各种伪造消息攻击,然后使用模糊集合理论,对恶意结点的攻击行为进行分析和识别,并采用相应的防范策略来应对这些攻击,最终缓解恶意结点对路由效率的影响。