ssprove

Tech stack & purpose

SSProve is a foundational framework for modular cryptographic proofs built in Rocq (formerly Coq). The project provides a formalization corresponding to peer-reviewed research papers, with the extended journal version published at TOPLAS and a conference version that received a distinguished paper award at CSF 2021. The framework is built on a package-based abstraction that enables composable cryptographic security proofs through sequential and parallel composition operations, and includes a probabilistic relational program logic for reasoning about game-based security definitions. The tech stack centers on Rocq as the proof assistant, along with supporting libraries including Equations, Mathcomp, Mathcomp analysis, Mathcomp word, Rocq Extructures, and Rocq Deriving, with installation available via either opam or nix package managers.

Community & reference links

• TYPES'21
• CSF'21
• Rocq Workshop '21

Languages

Contributors

• Théo Winterhalter899 commits
• 
  4ever2128 commits · 10 followers
• antoine_vanmuylder107 commits
• Carmine Abate86 commits
• Markus Krabbe Larsen84 commits
• 
  Kenji Maillard67 commits · 52 followers
• 
  Ramkumar Ramachandra65 commits · 295 followers
• Philipp G. Haselwarter49 commits
• Sebastian Ertel47 commits
• 
  E. Rivas46 commits · 0 followers
• 
  ErVinuelas40 commits · 6 followers
• Antoine Van Muylder39 commits
• Nikolaj Sidorenco36 commits
• Catalin Hritcu20 commits
• Theo Laurent19 commits
• Bas Spitters14 commits
• 
  dependabot[bot]5 commits · 0 followers
• 
  Pierre Roux4 commits · 18 followers
• 
  Quentin VERMANDE4 commits · 6 followers
• 
  Kazuhiko Sakaguchi2 commits · 199 followers
• MarkusKL1 commits
• Sebastian1 commits
• 
  Lasse Letager Hansen1 commits · 16 followers
• carmine1 commits
• 
  Vincent Laporte1 commits · 79 followers
• Adrian Bibby Walther1 commits