
Formalizing np1sec using Tamarin and other FM (see https://github.com/equalitie/np1sec)
Ricerca sulla dimostrazione della riservatezza della chiave di gruppo nella parte di scambio di chiavi di gruppo di (n+1)sec, con alcune limitazioni, come ad esempio avere solo 3 partecipanti. Questo lavoro è stato svolto da Alex Balducci e Andy Lee.
Il documento principale è gkep_normxorm_simplified_writeup.txt. Contiene riferimenti ai due documenti di "prova manuale" e a gkep_normxorm_simplified_cleaned.spthy, che è l'input per Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy è l'output di Tamarin.
Vedi anche useful_results.txt