nccgroup/formal_np1secFormalizing np1sec using Tamarin and other FM (see https://github.com/equalitie/np1sec)
Recherche sur la preuve de la confidentialité de la clé de groupe dans la partie échange de clé de groupe de (n+1)sec, avec certaines limitations, comme le fait de n'avoir que 3 participants. Ce travail a été réalisé par Alex Balducci et Andy Lee.
Le document principal est gkep_normxorm_simplified_writeup.txt. Il contient des références aux deux documents de « preuve à la main » et à gkep_normxorm_simplified_cleaned.spthy, qui est l'entrée de Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy est la sortie de Tamarin.
Voir aussi useful_results.txt
