nccgroup/formal_np1secصياغة np1sec باستخدام Tamarin وطرق رسمية أخرى (انظر https://github.com/equalitie/np1sec)
بحث حول إثبات سرية المفتاح الجماعي في جزء تبادل المفاتيح الجماعية لبروتوكول (n+1)sec، مع بعض القيود مثل وجود 3 مشاركين فقط. تم هذا العمل بواسطة Alex Balducci و Andy Lee.
المستند الرئيسي هو gkep_normxorm_simplified_writeup.txt. يحتوي على مراجع لمستندَي «الإثبات اليدوي» وgkep_normxorm_simplified_cleaned.spthy، وهو المدخل إلى Tamarin. أما GKEP_3_normxorm_simplified_cleaned_proof.spthy فهو ناتج Tamarin.
انظر أيضًا إلى useful_results.txt
