Research into proving the confidentiality of the group key in the group key exchange part of (n+1)sec, with certain limitations such as having only 3 participants. This work was done by Alex Balducci and Andy Lee.
The main document is gkep_normxorm_simplified_writeup.txt. It contains references to the two "proof by hand” documents and gkep_normxorm_simplified_cleaned.spthy, which is the input to Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy is the output of Tamarin.
See also useful_results.txt