On the public citation graph
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
0 signed · 94 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/11541868_4openalex-snapshot
Mechanized Metatheory for the Masses: The PoplMark Challenge
inferredcites →https://doi.org/10.1007/11761679_25openalex-snapshot
The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
inferredcites →https://doi.org/10.1007/11783596_6openalex-snapshot
Proofs of Randomized Algorithms in Coq
inferredcites →https://doi.org/10.1007/978-1-4757-4721-8openalex-snapshot
Categories for the Working Mathematician
inferredcites →https://doi.org/10.1007/978-3-030-03332-3_9openalex-snapshot
State Separation for Code-Based Game-Playing Proofs
inferredcites →https://doi.org/10.1007/978-3-030-51054-1_1openalex-snapshot
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
inferredcites →https://doi.org/10.1007/978-3-030-99253-8_9openalex-snapshot
Categorical composable cryptography
inferredcites →https://doi.org/10.1007/978-3-031-22963-3_21openalex-snapshot
Key-Schedule Security for the TLS 1.3 Standard
inferredcites →https://doi.org/10.1007/978-3-319-65127-9_22openalex-snapshot
Automated Cryptographic Analysis of the Pedersen Commitment Scheme
inferredcites →https://doi.org/10.1007/978-3-319-72044-9_14openalex-snapshot
Generic Hoare Logic for Order-Enriched Effects with Exceptions
inferredcites →https://doi.org/10.1007/978-3-319-96881-0_1openalex-snapshot
Simplifying Game-Based Definitions
inferredcites →https://doi.org/10.1007/978-3-642-00590-9_7openalex-snapshot
Handlers of Algebraic Effects
inferredcites →https://doi.org/10.1007/978-3-642-14303-8openalex-snapshot
Efficient Secure Two-Party Protocols: Techniques and Constructions
inferredcites →https://doi.org/10.1007/978-3-642-19718-5_1openalex-snapshot
Verified Software Toolchain
inferredcites →https://doi.org/10.1007/978-3-642-22792-9_5openalex-snapshot
Computer-Aided Security Proofs for the Working Cryptographer
inferredcites →https://doi.org/10.1007/978-3-642-25379-9_12openalex-snapshot
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
inferredcites →https://doi.org/10.1007/978-3-642-25379-9_27openalex-snapshot
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
inferredcites →https://doi.org/10.1007/978-3-642-27375-9_3openalex-snapshot
Constructive Cryptography – A New Paradigm for Security Definitions and Proofs
inferredcites →https://doi.org/10.1007/978-3-642-37075-5_10openalex-snapshot
Preorders on Monads and Coalgebraic Simulations
inferredcites →https://doi.org/10.1007/978-3-662-44381-1_14openalex-snapshot
Proving the TLS Handshake Secure (As It Is)
inferredcites →https://doi.org/10.1007/978-3-662-46666-7_4openalex-snapshot
The Foundational Cryptography Framework
inferredcites →https://doi.org/10.1007/978-3-662-48899-7_27openalex-snapshot
Relational Reasoning via Probabilistic Coupling
inferredcites →https://doi.org/10.1007/bf00196725openalex-snapshot
Efficient signature generation by smart cards
inferredcites →https://doi.org/10.1007/bfb0092872openalex-snapshot
A categorical approach to probability theory
inferredcites →https://doi.org/10.1007/s00145-013-9167-4openalex-snapshot
Subtleties in the Definition of IND-CCA: When and How Should Challenge Decryption Be Disallowed?
inferredcites →https://doi.org/10.1007/s00145-019-09341-zopenalex-snapshot
CryptHOL: Game-Based Proofs in Higher-Order Logic
inferredcites →https://doi.org/10.1007/s10817-008-9097-2openalex-snapshot
Nominal Techniques in Isabelle/HOL
inferredcites →https://doi.org/10.1007/s10817-018-9458-4openalex-snapshot
Hammer for Coq: Automation for Dependent Type Theory
inferredcites →https://doi.org/10.1007/s10817-020-09581-wopenalex-snapshot
Formalising Σ-Protocols and Commitment Schemes using CryptHOL.
inferredcites →https://doi.org/10.1016/0890-5401(92)90008-4openalex-snapshot
A calculus of mobile processes, I
inferredcites →https://doi.org/10.1016/j.ic.2016.02.008openalex-snapshot
A mathematical theory of resources
inferredcites →https://doi.org/10.1016/j.jlamp.2014.02.001openalex-snapshot
Programming with algebraic effects and handlers
inferredcites →https://doi.org/10.1017/s0956796819000170openalex-snapshot
POPLMark reloaded: Mechanizing proofs by logical relations
inferredcites →https://doi.org/10.1023/a:1023064908962openalex-snapshot
Algebraic Operations and Generic Effects
inferredcites →https://doi.org/10.1109/csf.2019.00018openalex-snapshot
Formalizing Constructive Cryptography using CryptHOL
inferredcites →https://doi.org/10.1109/csf.2019.00019openalex-snapshot
EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security
inferredcites →https://doi.org/10.1109/csf51468.2021.00048openalex-snapshot
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
inferredcites →https://doi.org/10.1109/csf51468.2021.00049openalex-snapshot
Mechanised Models and Proofs for Distance-Bounding
inferredcites →https://doi.org/10.1109/csf51468.2021.00050openalex-snapshot
Formal security analysis of MPC-in-the-head zero-knowledge protocols
inferredcites →https://doi.org/10.1109/csf54842.2022.9919663openalex-snapshot
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
inferredcites →https://doi.org/10.1109/csf54842.2022.9919671openalex-snapshot
Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox
inferredcites →https://doi.org/10.1109/lics.1989.39155openalex-snapshot
Computational lambda-calculus and monads
inferredcites →https://doi.org/10.1109/sp.2006.1openalex-snapshot
A computationally sound mechanized prover for security protocols
inferredcites →https://doi.org/10.1109/sp.2017.58openalex-snapshot
Implementing and Proving the TLS 1.3 Record Layer
inferredcites →https://doi.org/10.1109/sp.2019.00005openalex-snapshot
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises
inferredcites →https://doi.org/10.1109/sp40000.2020.00028openalex-snapshot
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
inferredcites →https://doi.org/10.1109/sp40001.2021.00008openalex-snapshot
SoK: Computer-Aided Cryptography
inferredcites →https://doi.org/10.1109/sp40001.2021.00046openalex-snapshot
High-Assurance Cryptography in the Spectre Era
inferredcites →https://doi.org/10.1109/sp46214.2022.9833678openalex-snapshot
Security Analysis of the MLS Key Derivation
inferredcites →https://doi.org/10.1137/s0097539702403773openalex-snapshot
Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack
inferredcites →https://doi.org/10.1145/1480881.1480894openalex-snapshot
Formal certification of code-based cryptographic proofs
inferredcites →https://doi.org/10.1145/1866307.1866350openalex-snapshot
Computational indistinguishability logic
inferredcites →https://doi.org/10.1145/199448.199528openalex-snapshot
Monad transformers and modular interpreters
inferredcites →https://doi.org/10.1145/2046707.2046746openalex-snapshot
Modular code-based cryptographic verification
inferredcites →https://doi.org/10.1145/2508859.2516663openalex-snapshot
Fully automated analysis of padding-based encryption in the computational model
inferredcites →https://doi.org/10.1145/2810103.2813697openalex-snapshot
Automated Proofs of Pairing-Based Cryptography
inferredcites →https://doi.org/10.1145/2837614.2837655openalex-snapshot
Dependent types and multi-monadic effects in F*
inferredcites →https://doi.org/10.1145/3133956.3133974openalex-snapshot
Verified Correctness and Security of mbedTLS HMAC-DRBG
inferredcites →https://doi.org/10.1145/3314221.3314607openalex-snapshot
ILC: a calculus for composable, computational cryptography
inferredcites →https://doi.org/10.1145/3319535.3354228openalex-snapshot
A Machine-Checked Proof of Security for AWS Key Management Service
inferredcites →https://doi.org/10.1145/3319535.3363211openalex-snapshot
Machine-Checked Proofs for Cryptographic Standards
inferredcites →https://doi.org/10.1145/3371072openalex-snapshot
The next 700 relational program logics
inferredcites →https://doi.org/10.1145/3460120.3484548openalex-snapshot
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
inferredcites →https://doi.org/10.1145/3460120.3484771openalex-snapshot
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
inferredcites →https://doi.org/10.1145/3474834openalex-snapshot
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
inferredcites →https://doi.org/10.1145/3548606.3560689openalex-snapshot
Enforcing Fine-grained Constant-time Policies
inferredcites →https://doi.org/10.1145/3554342openalex-snapshot
Repository for Article 'A Core Calculus for Equational Proofs of Cryptographic Protocols'
inferredcites →https://doi.org/10.1145/3636501.3636961openalex-snapshot
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
inferredcites →https://doi.org/10.17487/rfc8446openalex-snapshot
The Transport Layer Security (TLS) Protocol Version 1.3
inferredcites →https://doi.org/10.17487/rfc9420openalex-snapshot
The Messaging Layer Security (MLS) Protocol
inferredcites →https://doi.org/10.2168/lmcs-11(1:3)2015openalex-snapshot
Monads need not be endofunctors
inferredcites →https://doi.org/10.7551/mitpress/2319.001.0001openalex-snapshot
The Definition of Standard ML
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/978-3-031-66997-2_8openalex-snapshot
Formalizing Coppersmith’s Method in Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/978-3-031-86695-1_7openalex-snapshot
hax: Verifying Security-Critical Rust Software Using Multiple Provers
inferred← citeshttps://doi.org/10.1007/978-981-95-3585-9_3openalex-snapshot
A Formal Foundation for Equational Reasoning on Probabilistic Programs
inferred← citeshttps://doi.org/10.1016/j.compeleceng.2026.110971openalex-snapshot
From hardness assumptions to energy-secure protocols: A systematic survey of Euclidean lattice-based cryptography
inferred← citeshttps://doi.org/10.1017/s0956796822000077openalex-snapshot
Extracting functional programs from Coq, in Coq
inferred← citeshttps://doi.org/10.1038/s41598-025-89208-5openalex-snapshot
A Dickson polynomial based group key agreement authentication scheme for ensuring conditional privacy preservation and traceability in VANETs
inferred← citeshttps://doi.org/10.1109/conisoft63288.2024.00036openalex-snapshot
Secure Cryptography Usage in Software Development: A Systematic Literature Review
inferred← citeshttps://doi.org/10.1109/csf61375.2024.00015openalex-snapshot
Dealing with Dynamic Key Compromise in Crypto Verif
inferred← citeshttps://doi.org/10.1109/csf64896.2025.00038openalex-snapshot
Nominal State-Separating Proofs
inferred← citeshttps://doi.org/10.1109/csf68417.2026.00031openalex-snapshot
Composing Hybrid Arguments in Nominal-SSProve
inferred← citeshttps://doi.org/10.1145/3497775.3503675openalex-snapshot
A verified algebraic representation of cairo program execution
inferred← citeshttps://doi.org/10.1145/3636501.3636961openalex-snapshot
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
inferred← citeshttps://doi.org/10.1145/3704877openalex-snapshot
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
inferred← citeshttps://doi.org/10.1145/3805702openalex-snapshot
Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.