(n+1)sec のグループ鍵交換部分におけるグループ鍵の機密性の証明に関する研究。参加者が3名のみであるといった一定の制約があります。この研究は Alex Balducci と Andy Lee によって行われました。
メイン文書は gkep_normxorm_simplified_writeup.txt です。この文書には、「手作業による証明」(proof by hand) と呼ばれる2つの文書と、Tamarin への入力である gkep_normxorm_simplified_cleaned.spthy への参照が含まれています。GKEP_3_normxorm_simplified_cleaned_proof.spthy は Tamarin の出力です。
関連情報として useful_results.txt も参照してください。