针对 Diffie-Hellman 的按需 enrichment 协议分析（扩展版）

按需 enrichment（enrich-by-need）协议分析是一种符号化协议分析风格，刻画了扩展给定场景的协议的所有执行。实际上，它计算出协议在该场景下可达到的最强安全目标。CPSA（Cryptographic Protocol Shapes Analyzer，密码协议形状分析器）实现了按需 enrichment 协议分析。在本文中，我们描述如何以按需 enrichment 风格分析使用 Diffie-Hellman 机制进行密钥协商（DH）的协议。DH 虽广泛应用，但因其代数结构而对协议分析构成挑战。DH 本质上涉及域与循环群，这并不契合符号化协议分析的标准基础框架。相比之下，我们通过一个代数上自然的模型来证明我们的分析。该基础使扩展的 CPSA 实现可靠。此外，它提供信息丰富且高效的结果。附录解释了在我们的框架中如何高效地完成合一（unification）。