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