随着目前移动通信技术的飞速发展以及智能移动终端的普及,即时通讯软件已成为大部分用户在生活和工作中不可或缺的一部分。由于情报部门进行的大规模监视行为以及层出不穷的数据泄露事件促使许多人使用替代解决方案以用来保护他们在互联网上的通信的安全性和隐私性。因此多款国外即时通讯软件都使用了端到端加密算法。端到端加密没有采用服务器加解密消息,而是在通讯双方使用终端上进行消息的加密或者解密,服务器仅仅负责传输消息,通信服务商都没有办法查看通信内容。本文基于Android逆向分析技术对广泛使用的端到端加密即时通讯应用进行逆向工程,从技术层面研究了端到端加密即时通讯软件如何处理用户之间的消息,端到端加密流程以及端到端加密算法的安全属性。论文主要工作如下:(1)研究Android平台下的相关知识以及逆向分析技术,提出了一套逆向分析方案,该方案以原始APK文件为起点,逆向过程从APK重打包重签名技术、静态分析技术、无源码调试技术、动态插桩技术这四个角度展开对于Android系统的两个代码层次(Java层代码和Native层代码)进行分析。(2)根据提出的逆向分析方案构建逆向分析系统,整个逆向系统分为三个模块,静态分析模块、动态调试模块、动态插桩模块,整个系统兼顾逆向分析Java层代码和Native层代码,侧重于对Native层代码的分析。整个逆向分析系统可以在保证精确性和准确性的条件下获取函数级数据如函数运行情况、函数调用情况、寄存器内容等,从而确定与特定功能相关的函数位置以及函数运行情况,避免对与目标无关代码的分析。(3)利用逆向分析系统分析两款常用的端到端加密即时通讯软件,分析选用的两款即时通讯软件为Signal和Xxxx,根据逆向分析结果总结出应用中的端到端加密流程以及其中涉及到的密钥调度情况。通过逆向分析开源软件Signal验证了逆向分析方案的可行性,从而更加有效的逆向分析Xxxx。两款即时通讯软件端到端加密流程均包括四个阶段:注册阶段、会话建立阶段、非对称棘轮更新阶段、对称棘轮更新阶段,经过四个阶段的处理最终实现即时通讯的端到端加密。两款应用中的端到端加密算法均主要包括X3DH算法、双棘轮加密算法,但其中算法实现细节有不同之处。对于非对称棘轮更新阶段,Signal应用会在收到对方非对称棘轮公钥后进行连续的两次棘轮步进,第一次棘轮步进用于更新出接收链,紧接着第二次棘轮步进更新出发送链;而Xxxx应用收到带非对称棘轮的消息后仅仅会用非对称棘轮更新出接收轮次密钥,直到接下来由消息接收方变为消息发送方时才更新出发送轮次密钥。对于对称棘轮更新阶段,Signal应用中通过密钥生成链派生出对称密钥的方式以更新对称棘轮,而Xxxx应用通过两次Salsa20流加密算法保证消息明文的私密性。(4)为了验证端到端加密算法的各种安全属性,利用应用pi演算语言模拟逆向分析得出的端到端加密流程,并利用形式化验证工具Proverif设计验证了一系列安全属性,如消息的私密性、完整性、不可区分性、前向安全性、未来安全性、身份认证、重放攻击。形式化验证结果表明在保证初始身份密钥正确的情况下,Signal和Xxxx中的端到端加密算法能够保证消息的私密性、完整性、前向安全性、未来安全性并且可以延续正确的身份认证,但是仅仅靠端到端加密算法无法保证消息的不可区分性。