formal_np1sec

(n+1)sec의 그룹 키 교환 부분에서 그룹 키의 기밀성을 증명하는 연구로, 참가자가 3명뿐이라는 등의 특정 제한 사항이 있습니다. 이 작업은 Alex Balducci와 Andy Lee가 수행했습니다.

주요 문서는 gkep_normxorm_simplified_writeup.txt입니다. 여기에는 두 개의 "수기 증명" 문서와 Tamarin의 입력값인 gkep_normxorm_simplified_cleaned.spthy에 대한 참조가 포함되어 있습니다. GKEP_3_normxorm_simplified_cleaned_proof.spthy는 Tamarin의 출력값입니다.

useful_results.txt도 참조하세요.