
Formalizing np1sec using Tamarin and other FM (see https://github.com/equalitie/np1sec)
Investigación sobre la demostración de la confidencialidad de la clave de grupo en la parte de intercambio de claves de grupo de (n+1)sec, con ciertas limitaciones como tener solo 3 participantes. Este trabajo fue realizado por Alex Balducci y Andy Lee.
El documento principal es gkep_normxorm_simplified_writeup.txt. Contiene referencias a los dos documentos de "prueba a mano” y a gkep_normxorm_simplified_cleaned.spthy, que es la entrada para Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy es la salida de Tamarin.
Véase también useful_results.txt