定理证明方法一般可用于证明协议的安全性，但难以发现协议的漏洞，并且在自动化方面弱于模型检测分析。

定理证明方法具有以下特点：

①用一集代数或者逻辑公式定义系统行为，构成系统行为集合，用一集公理和系统的行为，作为推理的基础公式集。

②所期望的系统行为和性质，描述成一组公式，称为定理。

③从基础公式集出发，进行定理证明过程，达到期望的结果。

经典的定理证明方法包括Paulson归纳证明方法和串空间模型方法。Paulson归纳证明方法利用高阶逻辑描述公式，对敌手能力进行归纳定义，对协议运行中敌手可获取的消息进行归纳定义。协议的安全性由定理描述，对定理的证明采用归纳法按步推理得到，使用定理证明器Isabelle证明协议安全性；Thayer等人提出的串空间模型方法借鉴了归纳的部分思想，其中对密码协议采用图的方法进行描述，定义串空间是由各种合法主体的串和敌手的串组成，串空间中用丛定义协议交互过程，用丛所满足的特性刻画安全属性，通常以定理的形式给出。定理证明方法相比模型检测方法自动化实现较为困难，但证明过程中部分可以实现自动化，此类自动证明系统称为定理证明器，定理证明器更加依赖人为的帮助，自动化和操作便捷性远没有模型检测工具高。常见的定理证明器有：Isabelle、HOL、PVS、CryptoVerif等。

定理证明分析是由公理、假设以及推理规则组成，此系统通常有两个刻画，一个是可靠性或相容性，另一个是完备性。前者是指系统证明出的每个定理都是语义正确的，后者指语义正确的定理都可以通过此系统推理出来。其中可靠性是每个系统需要具备的，因此相比逻辑分析方法和模型检测方法，定理证明分析方法虽然直观性一般且自动化实现困难，但分析出的结果往往更具有说服力。