nccgroup/formal_np1sec# Formalizando o np1sec usando Tamarin e outras FM (ver https://github.com/equalitie/np1sec)
Investigação sobre a prova da confidencialidade da chave de grupo na parte de troca de chave de grupo do (n+1)sec, com certas limitações, como ter apenas 3 participantes. Este trabalho foi realizado por Alex Balducci e Andy Lee.
O documento principal é gkep_normxorm_simplified_writeup.txt. Ele contém referências aos dois documentos de "prova manual" e a gkep_normxorm_simplified_cleaned.spthy, que é a entrada para o Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy é a saída do Tamarin.
Consulte também useful_results.txt
