
Formalisierung von np1sec mit Tamarin und anderen FM (siehe https://github.com/equalitie/np1sec)
Forschung zum Nachweis der Vertraulichkeit des Gruppenschlüssels im Gruppenschlüsselaustausch-Teil von (n+1)sec, mit bestimmten Einschränkungen wie nur 3 Teilnehmern. Diese Arbeit wurde von Alex Balducci und Andy Lee durchgeführt.
Das Hauptdokument ist gkep_normxorm_simplified_writeup.txt. Es enthält Verweise auf die beiden „Proof by Hand“-Dokumente und gkep_normxorm_simplified_cleaned.spthy, das die Eingabe für Tamarin ist. GKEP_3_normxorm_simplified_cleaned_proof.spthy ist die Ausgabe von Tamarin.
Siehe auch useful_results.txt