研究在 (n+1)sec 的组密钥交换部分中证明组密钥机密性的工作，存在某些限制，例如仅包含 3 个参与者。这项工作由 Alex Balducci 和 Andy Lee 完成。
主要文档是 gkep_normxorm_simplified_writeup.txt。其中引用了两份“手工证明”文档以及 gkep_normxorm_simplified_cleaned.spthy，后者是 Tamarin 的输入。GKEP_3_normxorm_simplified_cleaned_proof.spthy 是 Tamarin 的输出。
另见 useful_results.txt
