
Formalizing np1sec using Tamarin and other FM (see 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