nccgroup/formal_np1sec# Tamarin और अन्य FM का उपयोग करके np1sec को औपचारिक रूप देना (देखें https://github.com/equalitie/np1sec)
समूह कुंजी विनिमय भाग में (n+1)sec की समूह कुंजी की गोपनीयता सिद्ध करने पर शोध, कुछ सीमाओं के साथ जैसे केवल 3 प्रतिभागी होना। यह कार्य Alex Balducci और Andy Lee द्वारा किया गया था।
मुख्य दस्तावेज़ gkep_normxorm_simplified_writeup.txt है। इसमें दो "proof by hand” दस्तावेज़ों और gkep_normxorm_simplified_cleaned.spthy के संदर्भ हैं, जो Tamarin का इनपुट है। GKEP_3_normxorm_simplified_cleaned_proof.spthy Tamarin का आउटपुट है।
useful_results.txt भी देखें।
