formal_np1sec

Исследование, посвящённое доказательству конфиденциальности группового ключа в части обмена групповыми ключами протокола (n+1)sec, при определённых ограничениях, например, при участии только трёх участников. Эта работа выполнена Алексом Бальдуччи и Энди Ли.

Основной документ — gkep_normxorm_simplified_writeup.txt. В нём содержатся ссылки на два документа с «доказательством вручную» и на gkep_normxorm_simplified_cleaned.spthy, который является входными данными для Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy — это выходные данные Tamarin.

См. также useful_results.txt