On the public citation graph
A computationally sound mechanized prover for security protocols
0 signed · 232 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.1006/jcss.1999.1694openalex-snapshot
The Security of the Cipher Block Chaining Message Authentication Code
inferredcites →https://doi.org/10.1007/11523468_2openalex-snapshot
Probabilistic Polynomial-Time Semantics for a Protocol Security Logic
inferredcites →https://doi.org/10.1007/11523468_53openalex-snapshot
Computationally Sound Implementations of Equational Theories Against Passive Adversaries
inferredcites →https://doi.org/10.1007/11555827_22openalex-snapshot
Soundness of Formal Encryption in the Presence of Key-Cycles
inferredcites →https://doi.org/10.1007/11555827_9openalex-snapshot
Machine-Checked Security Proofs of Cryptographic Signature Schemes
inferredcites →https://doi.org/10.1007/11681878_20openalex-snapshot
Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols
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/11818175_32openalex-snapshot
Automated Security Proofs with Sequences of Games
inferredcites →https://doi.org/10.1007/3-540-36575-3_12openalex-snapshot
Handling Encryption in an Analysis for Secure Information Flow
inferredcites →https://doi.org/10.1007/3-540-45500-0_4openalex-snapshot
Formal Eavesdropping and Its Computational Interpretation
inferredcites →https://doi.org/10.1007/3-540-48119-2_43openalex-snapshot
Probabilistic Polynomial-Time Equivalence and Security Analysis
inferredcites →https://doi.org/10.1007/3-540-61042-1_43openalex-snapshot
Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR
inferredcites →https://doi.org/10.1007/978-3-540-24638-1_8openalex-snapshot
Soundness of Formal Encryption in the Presence of Active Adversaries
inferredcites →https://doi.org/10.1007/978-3-540-24727-2_33openalex-snapshot
Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols
inferredcites →https://doi.org/10.1007/978-3-540-25984-8_29openalex-snapshot
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model
inferredcites →https://doi.org/10.1007/978-3-540-30580-4_6openalex-snapshot
Password-Based Authenticated Key Exchange in the Three-Party Setting
inferredcites →https://doi.org/10.1007/978-3-540-31987-0_12openalex-snapshot
Computationally Sound, Automated Proofs for Security Protocols
inferredcites →https://doi.org/10.1007/978-3-540-31987-0_13openalex-snapshot
Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries
inferredcites →https://doi.org/10.1007/978-3-540-39650-5_16openalex-snapshot
Symmetric Authentication within a Simulatable Cryptographic Library
inferredcites →https://doi.org/10.1007/978-3-540-45187-7_22openalex-snapshot
Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus
inferredcites →https://doi.org/10.1007/978-3-642-81955-1_23openalex-snapshot
Simple Word Problems in Universal Algebras
inferredcites →https://doi.org/10.1007/bfb0055718openalex-snapshot
Relations among notions of security for public-key encryption schemes
inferredcites →https://doi.org/10.1007/s00145-001-0014-7openalex-snapshot
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
inferredcites →https://doi.org/10.1016/j.tcs.2005.03.003openalex-snapshot
A computational interpretation of Dolev–Yao adversaries
inferredcites →https://doi.org/10.1016/j.tcs.2005.10.044openalex-snapshot
A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols
inferredcites →https://doi.org/10.1016/s1571-0661(04)80968-xopenalex-snapshot
A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols
inferredcites →https://doi.org/10.1049/ip-ifs:20055073openalex-snapshot
Password-based authenticated key exchange in the three-party setting
inferredcites →https://doi.org/10.1109/32.481513openalex-snapshot
Prudent engineering practice for cryptographic protocols
inferredcites →https://doi.org/10.1109/csf.2007.16openalex-snapshot
Computationally Sound Mechanized Proofs of Correspondence Assertions
inferredcites →https://doi.org/10.1109/csfw.2004.1310742openalex-snapshot
Symmetric encryption in a simulatable Dolev-Yao style cryptographic library
inferredcites →https://doi.org/10.1109/csfw.2004.20openalex-snapshot
Symmetric encryption in a simulatable Dolev-Yao style cryptographic library
inferredcites →https://doi.org/10.1109/csfw.2006.10openalex-snapshot
Cryptographically Sound Theorem Proving
inferredcites →https://doi.org/10.1109/risp.1993.287633openalex-snapshot
A semantic model for authentication protocols
inferredcites →https://doi.org/10.1109/secpri.2004.1301316openalex-snapshot
Symmetric encryption in automatic analyses for con .dentiality against active adversaries
inferredcites →https://doi.org/10.1109/secpri.2004.1301317openalex-snapshot
Automatic proof of strong secrecy for security protocols
inferredcites →https://doi.org/10.1109/sfcs.1997.646128openalex-snapshot
A concrete security treatment of symmetric encryption
inferredcites →https://doi.org/10.1109/sfcs.2001.959888openalex-snapshot
Universally composable security: a new paradigm for cryptographic protocols
inferredcites →https://doi.org/10.1109/sp.2005.17openalex-snapshot
Relating Symbolic and Cryptographic Secrecy
inferredcites →https://doi.org/10.1109/sp.2006.1openalex-snapshot
A computationally sound mechanized prover for security protocols
inferredcites →https://doi.org/10.1145/1102120.1102126openalex-snapshot
Secrecy types for a simulatable cryptographic library
inferredcites →https://doi.org/10.1145/1180405.1180450openalex-snapshot
Computationally sound secrecy proofs by mechanized flow analysis
inferredcites →https://doi.org/10.1145/24592.24594openalex-snapshot
Efficient and timely mutual authentication
inferredcites →https://doi.org/10.1145/288090.288117openalex-snapshot
A probabilistic poly-time framework for protocol analysis
inferredcites →https://doi.org/10.1145/358722.358740openalex-snapshot
Timestamps in key distribution protocols
inferredcites →https://doi.org/10.1145/359657.359659openalex-snapshot
Using encryption for authentication in large networks of computers
inferredcites →https://doi.org/10.1145/948109.948140openalex-snapshot
A composable cryptographic library with nested operations
inferredcites →https://doi.org/10.3233/jcs-2004-12105openalex-snapshot
Completeness theorems for the Abadi–Rogaway language of encrypted expressions1
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/11523468_53openalex-snapshot
Computationally Sound Implementations of Equational Theories Against Passive Adversaries
inferred← citeshttps://doi.org/10.1007/11787006_22openalex-snapshot
A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
inferred← citeshttps://doi.org/10.1007/11818175_32openalex-snapshot
Automated Security Proofs with Sequences of Games
inferred← citeshttps://doi.org/10.1007/11863908_23openalex-snapshot
Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos
inferred← citeshttps://doi.org/10.1007/11863908_25openalex-snapshot
Limits of the BRSIM/UC Soundness of Dolev-Yao Models with Hashes
inferred← citeshttps://doi.org/10.1007/978-0-387-87969-7_10openalex-snapshot
Complementing Computational Protocol Analysis
inferred← citeshttps://doi.org/10.1007/978-3-030-04762-7_2openalex-snapshot
Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)
inferred← citeshttps://doi.org/10.1007/978-3-030-61638-0_1openalex-snapshot
Towards a Formally Verified Implementation of the MimbleWimble Cryptocurrency Protocol
inferred← citeshttps://doi.org/10.1007/978-3-030-65277-7_8openalex-snapshot
Verifpal: Cryptographic Protocol Analysis for the Real World
inferred← citeshttps://doi.org/10.1007/978-3-030-71522-9_1673openalex-snapshot
Formal Verification of Cryptosystems
inferred← citeshttps://doi.org/10.1007/978-3-030-90636-8_1openalex-snapshot
Learning Assumptions for Verifying Cryptographic Protocols Compositionally
inferred← citeshttps://doi.org/10.1007/978-3-030-99527-0_10openalex-snapshot
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
inferred← citeshttps://doi.org/10.1007/978-3-031-08143-9_1openalex-snapshot
Formal Methods for Socio-technical Security
inferred← citeshttps://doi.org/10.1007/978-3-031-22295-5_13openalex-snapshot
Automatic Implementations Synthesis of Secure Protocols and Attacks from Abstract Models
inferred← citeshttps://doi.org/10.1007/978-3-319-06320-1_12openalex-snapshot
Automated Proof for Authorization Protocols of TPM 2.0 in Computational Model
inferred← citeshttps://doi.org/10.1007/978-3-319-17533-1_35openalex-snapshot
A Framework for Analyzing Verifiability in Traditional and Electronic Exams
inferred← citeshttps://doi.org/10.1007/978-3-319-22969-0_4openalex-snapshot
Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications
inferred← citeshttps://doi.org/10.1007/978-3-319-49109-7_90openalex-snapshot
Security Analysis of OpenID Connect Protocol with Cryptoverif in the Computational Model
inferred← citeshttps://doi.org/10.1007/978-3-319-62033-6_15openalex-snapshot
SMAPs: Short Message Authentication Protocols
inferred← citeshttps://doi.org/10.1007/978-3-540-68746-7_9openalex-snapshot
Modeling and Analysis of Security Protocols Using Role Based Specifications and Petri Nets
inferred← citeshttps://doi.org/10.1007/978-3-540-70630-4_6openalex-snapshot
Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover
inferred← citeshttps://doi.org/10.1007/978-3-540-74810-6_1openalex-snapshot
Security Protocols: Principles and Calculi
inferred← citeshttps://doi.org/10.1007/978-3-540-74835-9_40openalex-snapshot
Adaptive Soundness of Static Equivalence
inferred← citeshttps://doi.org/10.1007/978-3-540-75227-1_4openalex-snapshot
Game-Based Criterion Partition Applied to Computational Soundness of Adaptive Security
inferred← citeshttps://doi.org/10.1007/978-3-540-77050-3_9openalex-snapshot
On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography
inferred← citeshttps://doi.org/10.1007/978-3-540-78663-4_20openalex-snapshot
Application of Dependency Graphs to Security Protocol Analysis
inferred← citeshttps://doi.org/10.1007/978-3-540-88733-1_21openalex-snapshot
Threshold Homomorphic Encryption in the Universally Composable Cryptographic Library
inferred← citeshttps://doi.org/10.1007/978-3-540-89439-1_26openalex-snapshot
A Formal Language for Cryptographic Pseudocode
inferred← citeshttps://doi.org/10.1007/978-3-642-02273-9_29openalex-snapshot
The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
inferred← citeshttps://doi.org/10.1007/978-3-642-02658-4_5openalex-snapshot
Models and Proofs of Protocol Security: A Progress Report
inferred← citeshttps://doi.org/10.1007/978-3-642-10772-6_6openalex-snapshot
On Secure Implementation of an IHE XUA-Based Protocol for Authenticating Healthcare Professionals
inferred← citeshttps://doi.org/10.1007/978-3-642-11512-7_19openalex-snapshot
Automated Proofs for Asymmetric Encryption
inferred← citeshttps://doi.org/10.1007/978-3-642-12459-4_10openalex-snapshot
Secure Information Flow for Distributed Systems
inferred← citeshttps://doi.org/10.1007/978-3-642-12459-4_19openalex-snapshot
A User Interface for a Game-Based Protocol Verification Tool
inferred← citeshttps://doi.org/10.1007/978-3-642-14992-4_16openalex-snapshot
How to Evaluate the Security of Real-Life Cryptographic Protocols?
inferred← citeshttps://doi.org/10.1007/978-3-642-15497-3_10openalex-snapshot
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Σ-Protocols
inferred← citeshttps://doi.org/10.1007/978-3-642-15497-3_21openalex-snapshot
Modeling and Analyzing Security in the Presence of Compromising Adversaries
inferred← citeshttps://doi.org/10.1007/978-3-642-20920-8_3openalex-snapshot
A Symbolic Logic with Exact Bounds for Cryptographic Protocols
inferred← citeshttps://doi.org/10.1007/978-3-642-22792-9_5openalex-snapshot
Computer-Aided Security Proofs for the Working Cryptographer
inferred← citeshttps://doi.org/10.1007/978-3-642-24073-7_1openalex-snapshot
Introduction of Cryptographic Protocols
inferred← citeshttps://doi.org/10.1007/978-3-642-24073-7_4openalex-snapshot
Informal Analysis Schemes of Cryptographic Protocols
inferred← citeshttps://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
inferred← citeshttps://doi.org/10.1007/978-3-642-27739-9_1673-1openalex-snapshot
Formal Verification of Cryptosystems
inferred← citeshttps://doi.org/10.1007/978-3-642-27901-0_9openalex-snapshot
A Computational Indistinguishability Logic for the Bounded Storage Model
inferred← citeshttps://doi.org/10.1007/978-3-642-29093-0_18openalex-snapshot
e-Health for Rural Areas in Developing Countries: Lessons from the Sebokeng Experience
inferred← citeshttps://doi.org/10.1007/978-3-642-29889-9_7openalex-snapshot
A Study on Computational Formal Verification for Practical Cryptographic Protocol: The Case of Synchronous RFID Authentication
inferred← citeshttps://doi.org/10.1007/978-3-642-33167-1_33openalex-snapshot
Decision Procedures for Simulatability
inferred← citeshttps://doi.org/10.1007/978-3-642-33704-8_6openalex-snapshot
A Vulnerability in the UMTS and LTE Authentication and Key Agreement Protocols
inferred← citeshttps://doi.org/10.1007/978-3-642-38574-2_6openalex-snapshot
Tractable Inference Systems: An Extension with a Deducibility Predicate
inferred← citeshttps://doi.org/10.1007/978-3-642-54792-8_12openalex-snapshot
Extending and Applying a Framework for the Cryptographic Verification of Java Programs
inferred← citeshttps://doi.org/10.1007/978-3-662-44893-9_14openalex-snapshot
Practical Authentication Protocols for Protecting and Sharing Sensitive Information on Mobile Devices
inferred← citeshttps://doi.org/10.1007/978-3-662-46803-6_23openalex-snapshot
Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols
inferred← citeshttps://doi.org/10.1007/978-3-662-48899-7_15openalex-snapshot
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
inferred← citeshttps://doi.org/10.1007/978-3-662-49896-5_29openalex-snapshot
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model
inferred← citeshttps://doi.org/10.1007/978-3-662-53015-3_14openalex-snapshot
Design in Type-I, Run in Type-III: Fast and Scalable Bilinear-Type Conversion Using Integer Programming
inferred← citeshttps://doi.org/10.1007/978-981-10-7080-8_11openalex-snapshot
A Dictionary Sequence Model to Analyze the Security of Protocol Implementations at the Source Code Level
inferred← citeshttps://doi.org/10.1007/978-981-95-5096-8_5openalex-snapshot
How Hard can it be to Formalize a Proof?
inferred← citeshttps://doi.org/10.1007/s10207-007-0040-zopenalex-snapshot
Limits of the BRSIM/UC soundness of Dolev–Yao-style XOR
inferred← citeshttps://doi.org/10.1007/s10207-011-0125-6openalex-snapshot
Cryptographically sound security proofs for basic and public-key Kerberos
inferred← citeshttps://doi.org/10.1007/s10626-007-0032-1openalex-snapshot
Analyzing Security Protocols Using Time-Bounded Task-PIOAs
inferred← citeshttps://doi.org/10.1007/s10817-010-9186-xopenalex-snapshot
Automated Proofs for Asymmetric Encryption
inferred← citeshttps://doi.org/10.1007/s10817-010-9187-9openalex-snapshot
A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems
inferred← citeshttps://doi.org/10.1007/s10817-019-09530-2openalex-snapshot
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
inferred← citeshttps://doi.org/10.1007/s11416-007-0063-zopenalex-snapshot
Static analysis by abstract interpretation: application to the detection of heap overflows
inferred← citeshttps://doi.org/10.1016/j.entcs.2006.07.009openalex-snapshot
Towards a Quantitative Analysis of Security Protocols
inferred← citeshttps://doi.org/10.1016/j.entcs.2007.10.009openalex-snapshot
A Probabilistic Scheduler for the Analysis of Cryptographic Protocols
inferred← citeshttps://doi.org/10.1016/j.entcs.2009.02.073openalex-snapshot
Rewriting Techniques in the Constraint Solver
inferred← citeshttps://doi.org/10.1016/j.entcs.2009.10.010openalex-snapshot
Modeling and Reasoning about an Attacker with Cryptanalytical Capabilities
inferred← citeshttps://doi.org/10.1016/j.ic.2007.05.002openalex-snapshot
The reactive simulatability (RSIM) framework for asynchronous systems
inferred← citeshttps://doi.org/10.1016/j.ic.2007.05.005openalex-snapshot
Breaking and fixing public-key Kerberos
inferred← citeshttps://doi.org/10.1016/j.ic.2008.12.005openalex-snapshot
Computationally sound implementations of equational theories against passive adversaries
inferred← citeshttps://doi.org/10.1017/s0960129510000265openalex-snapshot
The computational SLR: a logic for reasoning about computational indistinguishability
inferred← citeshttps://doi.org/10.1109/access.2020.3008230openalex-snapshot
An Enhanced Authentication Protocol for RFID Systems
inferred← citeshttps://doi.org/10.1109/access.2021.3063770openalex-snapshot
SGX-UAM: A Secure Unified Access Management Scheme With One Time Passwords via Intel SGX
inferred← citeshttps://doi.org/10.1109/csf.2007.16openalex-snapshot
Computationally Sound Mechanized Proofs of Correspondence Assertions
inferred← citeshttps://doi.org/10.1109/csf.2007.8openalex-snapshot
Approximated Computationally Bounded Simulation Relations for Probabilistic Automata
inferred← citeshttps://doi.org/10.1109/csf.2008.27openalex-snapshot
Refinement Types for Secure Implementations
inferred← citeshttps://doi.org/10.1109/csf.2009.18openalex-snapshot
Universally Composable Symmetric Encryption
inferred← citeshttps://doi.org/10.1109/csf.2011.8openalex-snapshot
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols
inferred← citeshttps://doi.org/10.1109/csf.2012.9openalex-snapshot
A Framework for the Cryptographic Verification of Java-Like Programs
inferred← citeshttps://doi.org/10.1109/csf.2014.19openalex-snapshot
Certified Synthesis of Efficient Batch Verifiers
inferred← citeshttps://doi.org/10.1109/csf.2015.13openalex-snapshot
Automatic Proofs of Privacy of Secure Multi-party Computation Protocols against Active Adversaries
inferred← citeshttps://doi.org/10.1109/csf.2017.9openalex-snapshot
Formal Computational Unlinkability Proofs of RFID Protocols
inferred← citeshttps://doi.org/10.1109/csf.2018.00009openalex-snapshot
Composition Theorems for CryptoVerif and Application to TLS 1.3
inferred← citeshttps://doi.org/10.1109/csf.2018.00018openalex-snapshot
Symbolic Security of Garbled Circuits
inferred← citeshttps://doi.org/10.1109/csf.2018.00033openalex-snapshot
Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR
inferred← citeshttps://doi.org/10.1109/csf.2019.00017openalex-snapshot
Symbolic Methods in Computational Cryptography Proofs
inferred← citeshttps://doi.org/10.1109/csf.2019.00018openalex-snapshot
Formalizing Constructive Cryptography using CryptHOL
inferred← citeshttps://doi.org/10.1109/csf51468.2021.00048openalex-snapshot
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
inferred← citeshttps://doi.org/10.1109/csf54842.2022.9919665openalex-snapshot
Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
inferred← citeshttps://doi.org/10.1109/csf61375.2024.00046openalex-snapshot
A Probabilistic Logic for Concrete Security
inferred← citeshttps://doi.org/10.1109/csf64896.2025.00006openalex-snapshot
Secrecy by Typing in the Computational Model
inferred← citeshttps://doi.org/10.1109/csf64896.2025.00019openalex-snapshot
SMT-Based Automation for Overwhelming Truth
inferred← citeshttps://doi.org/10.1109/csf68417.2026.00041openalex-snapshot
Computationally Sound Symbolic Cryptography in Lean
inferred← citeshttps://doi.org/10.1109/csfw.2006.10openalex-snapshot
Cryptographically Sound Theorem Proving
inferred← citeshttps://doi.org/10.1109/ias.2008.50openalex-snapshot
Automatic Verification of Simulatability in Security Protocols
inferred← citeshttps://doi.org/10.1109/iceccs.2014.11openalex-snapshot
Symbolic Analysis of an Electric Vehicle Charging Protocol
inferred← citeshttps://doi.org/10.1109/icfcc.2010.5497804openalex-snapshot
Automated security proof of the ElGamal encryption scheme
inferred← citeshttps://doi.org/10.1109/isecs.2009.45openalex-snapshot
Automatic Approach of Provable Security and its Application for OAEP+
inferred← citeshttps://doi.org/10.1109/isita.2008.4895465openalex-snapshot
Security verification for authentication and key exchange protocols
inferred← citeshttps://doi.org/10.1109/jcn.2006.6182794openalex-snapshot
Group key exchange over combined wired and wireless networks
inferred← citeshttps://doi.org/10.1109/lics.2013.66openalex-snapshot
From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic
inferred← citeshttps://doi.org/10.1109/pst.2018.8514201openalex-snapshot
Automated Proofs of Signatures using Bilinear Pairings
inferred← citeshttps://doi.org/10.1109/pst47121.2019.8949055openalex-snapshot
Exploring Automation in Proofs of Attribute-based Encryption in the Standard Model
inferred← citeshttps://doi.org/10.1109/sp.2009.17openalex-snapshot
Formally Certifying the Security of Digital Signature Schemes
inferred← citeshttps://doi.org/10.1109/sp.2013.37openalex-snapshot
Implementing TLS with Verified Cryptographic Security
inferred← citeshttps://doi.org/10.1109/sp.2015.21openalex-snapshot
How Secure and Quick is QUIC? Provable Security and Performance Analyses
inferred← citeshttps://doi.org/10.1109/sp.2017.63openalex-snapshot
A Framework for Universally Composable Diffie-Hellman Key Exchange
inferred← citeshttps://doi.org/10.1109/sp40001.2021.00078openalex-snapshot
An Interactive Prover for Protocol Verification in the Computational Model
inferred← citeshttps://doi.org/10.1109/sp46214.2022.9833777openalex-snapshot
Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities
inferred← citeshttps://doi.org/10.1109/sp54263.2024.00246openalex-snapshot
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
inferred← citeshttps://doi.org/10.1134/s0361768822080035openalex-snapshot
Optimization of ProVerif Programs for AKE Protocols
inferred← citeshttps://doi.org/10.1145/1180337.1180338openalex-snapshot
Securing the drop-box architecture for assisted living
inferred← citeshttps://doi.org/10.1145/1180405.1180450openalex-snapshot
Computationally sound secrecy proofs by mechanized flow analysis
inferred← citeshttps://doi.org/10.1145/1237500.1237504openalex-snapshot
Secure sessions for Web services
inferred← citeshttps://doi.org/10.1145/1250734.1250749openalex-snapshot
Static specification inference using predicate mining
inferred← citeshttps://doi.org/10.1145/1273442.1250749openalex-snapshot
Static specification inference using predicate mining
inferred← citeshttps://doi.org/10.1145/1368310.1368326openalex-snapshot
Computationally sound mechanized proofs for basic and public-key Kerberos
inferred← citeshttps://doi.org/10.1145/1455770.1455817openalex-snapshot
Towards automated proofs for asymmetric encryption schemes in the random oracle model
inferred← citeshttps://doi.org/10.1145/1455770.1455828openalex-snapshot
Cryptographically verified implementations for TLS
inferred← citeshttps://doi.org/10.1145/1480881.1480894openalex-snapshot
Formal certification of code-based cryptographic proofs
inferred← citeshttps://doi.org/10.1145/1594834.1480894openalex-snapshot
Formal certification of code-based cryptographic proofs
inferred← citeshttps://doi.org/10.1145/1653662.1653674openalex-snapshot
Computational soundness for key exchange protocols with symmetric encryption
inferred← citeshttps://doi.org/10.1145/1706299.1706350openalex-snapshot
Modular verification of security protocol code by typing
inferred← citeshttps://doi.org/10.1145/1707801.1706350openalex-snapshot
Modular verification of security protocol code by typing
inferred← citeshttps://doi.org/10.1145/1866307.1866350openalex-snapshot
Computational indistinguishability logic
inferred← citeshttps://doi.org/10.1145/1866307.1866351openalex-snapshot
Computationally sound verification of source code
inferred← citeshttps://doi.org/10.1145/1890028.1890031openalex-snapshot
Refinement types for secure implementations
inferred← citeshttps://doi.org/10.1145/1982185.1982527openalex-snapshot
Proving the security of ElGamal encryption via indistinguishability logic
inferred← citeshttps://doi.org/10.1145/2046707.2046745openalex-snapshot
Extracting and verifying cryptographic models from C protocol code by symbolic execution
inferred← citeshttps://doi.org/10.1145/2046707.2046746openalex-snapshot
Modular code-based cryptographic verification
inferred← citeshttps://doi.org/10.1145/2382196.2382272openalex-snapshot
Verified security of redundancy-free encryption from Rabin and RSA
inferred← citeshttps://doi.org/10.1145/2508859.2516663openalex-snapshot
Fully automated analysis of padding-based encryption in the computational model
inferred← citeshttps://doi.org/10.1145/2810103.2813697openalex-snapshot
Automated Proofs of Pairing-Based Cryptography
inferred← citeshttps://doi.org/10.1145/3190619.3190640openalex-snapshot
Formal verification of the W3C web authentication protocol
inferred← citeshttps://doi.org/10.1145/3243734.3243825openalex-snapshot
Symbolic Proofs for Lattice-Based Cryptography
inferred← citeshttps://doi.org/10.1145/3314221.3314607openalex-snapshot
ILC: a calculus for composable, computational cryptography
inferred← citeshttps://doi.org/10.1145/3319535.3339808openalex-snapshot
Are These Pairing Elements Correct?
inferred← citeshttps://doi.org/10.1145/3319535.3354228openalex-snapshot
A Machine-Checked Proof of Security for AWS Key Management Service
inferred← citeshttps://doi.org/10.1145/3372297.3417229openalex-snapshot
Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets
inferred← citeshttps://doi.org/10.1145/3372297.3417230openalex-snapshot
PPE Circuits: Formal Definition to Software Automation
inferred← citeshttps://doi.org/10.1145/3437992.3439917openalex-snapshot
A formal proof of PAC learnability for decision stumps
inferred← citeshttps://doi.org/10.1145/3460120.3484548openalex-snapshot
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
inferred← citeshttps://doi.org/10.1145/3460120.3484562openalex-snapshot
PPE Circuits for Rational Polynomials
inferred← citeshttps://doi.org/10.1145/3460120.3484567openalex-snapshot
EasyPQC: Verifying Post-Quantum Cryptography
inferred← citeshttps://doi.org/10.1145/3498685openalex-snapshot
Certifying derivation of state machines from coroutines
inferred← citeshttps://doi.org/10.1145/3571223openalex-snapshot
A Core Calculus for Equational Proofs of Cryptographic Protocols
inferred← citeshttps://doi.org/10.1145/3594735openalex-snapshot
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
inferred← citeshttps://doi.org/10.1201/b10928-10openalex-snapshot
Path-Aware Static Program Analyses for Specification Mining
inferred← citeshttps://doi.org/10.1504/ijsn.2014.060742openalex-snapshot
Security properties analysis in a TPM-based protocol
inferred← citeshttps://doi.org/10.15388/informatica.2007.193openalex-snapshot
An Integrative Framework to Protocol Analysis and Repair: Bellare–Rogaway Model + Planning + Model Checker
inferred← citeshttps://doi.org/10.1561/2500000001openalex-snapshot
Formal Models and Techniques for Analyzing Security Protocols: A Tutorial
inferred← citeshttps://doi.org/10.1561/9781601989031openalex-snapshot
Formal Models and Techniques for Analyzing Security Protocols: A Tutorial
inferred← citeshttps://doi.org/10.1587/transfun.e102.a.251openalex-snapshot
Fast and Scalable Bilinear-Type Conversion Method for Large Scale Crypto Schemes
inferred← citeshttps://doi.org/10.20868/upm.thesis.53392openalex-snapshot
Automated Analysis of Cryptographic Constructions
inferred← citeshttps://doi.org/10.3233/jcs-140508openalex-snapshot
Guiding a general-purpose C verifier to prove cryptographic protocols
inferred← citeshttps://doi.org/10.3233/jcs-15774openalex-snapshot
From qualitative to quantitative proofs of security properties using first-order conditional logic
inferred← citeshttps://doi.org/10.3233/jcs-191358openalex-snapshot
Verification of stateful cryptographic protocols with exclusive OR
inferred← citeshttps://doi.org/10.3233/jcs-2009-0392openalex-snapshot
Computational soundness of symbolic zero-knowledge proofs*
inferred← citeshttps://doi.org/10.3233/jcs-2009-389openalex-snapshot
Inductive trace properties for computational security
inferred← citeshttps://doi.org/10.3233/jcs-2010-0362openalex-snapshot
Calibrating the power of schedulers for probabilistic polynomial-time calculus
inferred← citeshttps://doi.org/10.32469/10355/79561openalex-snapshot
Machine-aided analysis of vote privacy using computationally complete symbolic attacker
inferred← citeshttps://doi.org/10.3390/cryptography10010013openalex-snapshot
Secure and Efficient Block Cipher Mode Design for Parallel Processing and Reliable Security
inferred← citeshttps://doi.org/10.34727/2020/isbn.978-3-85448-042-6_18openalex-snapshot
Automating Compositional Analysis of Authentication Protocols
inferred← citeshttps://doi.org/10.3929/ethz-a-009790675openalex-snapshot
Advancing automated security protocol verification
inferred← citeshttps://doi.org/10.4156/jdcta.vol5.issue1.36openalex-snapshot
Automatic Proofs of Deniable Authentication Protocols with a Probabilistic Polynomial Calculus in Computational Model
inferred← citeshttps://doi.org/10.48550/arxiv.1003.5383openalex-snapshot
Automatic analysis of distance bounding protocols
inferred← citeshttps://doi.org/10.48550/arxiv.1004.2522openalex-snapshot
How to prevent type-flaw and multi-protocol attacks on cryptographic protocols under Exclusive-OR
inferred← citeshttps://doi.org/10.48550/arxiv.1312.6532openalex-snapshot
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols
inferred← citeshttps://doi.org/10.48550/arxiv.1511.07536openalex-snapshot
A Symbolic Logic with Concrete Bounds for Cryptographic Protocols
inferred← citeshttps://doi.org/10.48550/arxiv.2007.14155openalex-snapshot
Local Variables and Quantum Relational Hoare Logic
inferred← citeshttps://doi.org/10.5220/0006901405370542openalex-snapshot
Attribute Based Signatures: The Case for Automation
inferred← citeshttps://doi.org/10.5753/sbc.5824.5.3openalex-snapshot
Introdução à Verificação Automática de Protocolos de Segurança com Scyther
inferred← citeshttps://doi.org/10.70675/19a9eee2z00e0z4d2dza27cz506b77c2769dopenalex-snapshot
Proof of security protocols revisited
inferred← citeshttps://doi.org/10.70675/1d79f521zac2fz4c89zae36z5157e79eec3fopenalex-snapshot
Approaches for analyzing security properties of smart objects
inferred← citeshttps://doi.org/10.70675/d68c77d4z020dz405ez86adz4690cf53b268openalex-snapshot
Preuves de protocoles cryptographiques : méthodes symboliques et attaquants puissants
showing the first 181 of 182 · page through all 182
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.