Skip to content
KitploitKITPLOIT
ToolsBlog
Submit
ToolsBlog
Submit

Hacking, PenTest, and Cybersecurity Tools for Your Security Arsenal!

Kitploit is a directory of hacking, cybersecurity, and pentesting tools. Discover the latest project updates to find vulnerabilities, analyze systems, automate testing, and strengthen your security.

··Feeds·Contact·Privacy·© 2026 Kitploit

Tool Directory

Categories

View all categories
Loading categories
formal_np1sec — Formalizing np1sec using Tamarin and other FM (see https://github.com/equalitie/np1sec) | Kitploit
Tools/GitHubGitHub/nccgroup/formal_np1sec
Static AnalysisCryptographyPapers & Research
GitHubnccgroup/formal_np1sec

formal_np1sec

Formalizing np1sec using Tamarin and other FM (see https://github.com/equalitie/np1sec)

View Repository
118 years agoNot yet reviewed

Most Popular

View all →

Discover the most used tools by our community.

Explore all tools

Browse our collection of tools

View all tools →
Share

Research into proving the confidentiality of the group key in the group key exchange part of (n+1)sec, with certain limitations such as having only 3 participants. This work was done by Alex Balducci and Andy Lee.

The main document is gkep_normxorm_simplified_writeup.txt. It contains references to the two "proof by hand” documents and gkep_normxorm_simplified_cleaned.spthy, which is the input to Tamarin. GKEP_3_normxorm_simplified_cleaned_proof.spthy is the output of Tamarin.

See also useful_results.txt

Download Tool