On the public citation graph

Automatically Verified Mechanized Proof of One-Encryption Key Exchange

https://doi.org/10.1109/csf.2012.8

0 signed · 78 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.

Claim with ORCID

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.

See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/11523468_2openalex-snapshot

Probabilistic Polynomial-Time Semantics for a Protocol Security Logic

inferredcites →https://doi.org/10.1007/11537311_32openalex-snapshot

A Type System for Computationally Secure Information Flow

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/11864219_17openalex-snapshot

Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols

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-45539-6_11openalex-snapshot

Authenticated Key Exchange Secure against Dictionary Attacks

inferredcites →https://doi.org/10.1007/3-540-45708-9_39openalex-snapshot

Security Proof for Partial-Domain Hash Signature Schemes

inferredcites →https://doi.org/10.1007/3-540-68339-9_34openalex-snapshot

The Exact Security of Digital Signatures-How to Sign with RSA and Rabin

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-77048-0_25openalex-snapshot

A Framework for Game-Based Security Proofs

inferredcites →https://doi.org/10.1007/978-3-540-77050-3_30openalex-snapshot

Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption

inferredcites →https://doi.org/10.1007/978-3-540-78663-4_20openalex-snapshot

Application of Dependency Graphs to Security Protocol Analysis

inferredcites →https://doi.org/10.1007/978-3-642-00730-9_23openalex-snapshot

On Formal Verification of Arithmetic-Based Cryptographic Primitives

inferredcites →https://doi.org/10.1007/978-3-642-01465-9_1openalex-snapshot

Formal Certification of ElGamal Encryption

inferredcites →https://doi.org/10.1007/978-3-642-11512-7_19openalex-snapshot

Automated Proofs for Asymmetric Encryption

inferredcites →https://doi.org/10.1007/978-3-642-12459-4_19openalex-snapshot

A User Interface for a Game-Based Protocol Verification Tool

inferredcites →https://doi.org/10.1007/978-3-642-16280-0_3openalex-snapshot

A Calculus for Game-Based Security Proofs

inferredcites →https://doi.org/10.1007/978-3-642-19074-2_13openalex-snapshot

Beyond Provable Security Verifiable IND-CCA Security of OAEP

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/bf00196908openalex-snapshot

On the Chor—Rivest knapsack cryptosystem

inferredcites →https://doi.org/10.1007/bfb0053428openalex-snapshot

Optimal asymmetric encryption

inferredcites →https://doi.org/10.1007/bfb0055732openalex-snapshot

Cryptanalysis of the Chor-Rivest cryptosystem

inferredcites →https://doi.org/10.1007/bfb0055741openalex-snapshot

On concrete security treatment of signatures derived from identification

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.1007/s00145-002-0133-9openalex-snapshot

OAEP Reconsidered

inferredcites →https://doi.org/10.1007/s00145-002-0204-yopenalex-snapshot

RSA-OAEP Is Secure under the RSA Assumption

inferredcites →https://doi.org/10.1007/s001450010005openalex-snapshot

Cryptanalysis of the Chor—Rivest Cryptosystem

inferredcites →https://doi.org/10.1007/s10817-010-9186-xopenalex-snapshot

Automated Proofs for Asymmetric Encryption

inferredcites →https://doi.org/10.1007/s10817-010-9187-9openalex-snapshot

A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

inferredcites →https://doi.org/10.1016/j.entcs.2006.11.044openalex-snapshot

Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

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/18.21214openalex-snapshot

A knapsack-type public key cryptosystem based on arithmetic in finite fields

inferredcites →https://doi.org/10.1109/csf.2007.16openalex-snapshot

Computationally Sound Mechanized Proofs of Correspondence Assertions

inferredcites →https://doi.org/10.1109/csf.2010.24openalex-snapshot

A Machine-Checked Formalization of Sigma-Protocols

inferredcites →https://doi.org/10.1109/csf.2012.8openalex-snapshot

Automatically Verified Mechanized Proof of One-Encryption Key Exchange

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/csfw.2006.9openalex-snapshot

Computationally Sound Compositional Logic for Key Exchange Protocols

inferredcites →https://doi.org/10.1109/lics.2008.36openalex-snapshot

Cryptographically-Sound Protocol-Model Abstractions

inferredcites →https://doi.org/10.1109/risp.1992.213269openalex-snapshot

Encrypted key exchange: password-based protocols secure against dictionary attacks

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.2001.959888openalex-snapshot

Universally composable security: a new paradigm for cryptographic protocols

inferredcites →https://doi.org/10.1109/sp.2009.17openalex-snapshot

Formally Certifying the Security of Digital Signature Schemes

inferredcites →https://doi.org/10.1109/tdsc.2007.1005openalex-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/1180337.1180341openalex-snapshot

Secure information flow with random assignment and encryption

inferredcites →https://doi.org/10.1145/1180405.1180450openalex-snapshot

Computationally sound secrecy proofs by mechanized flow analysis

inferredcites →https://doi.org/10.1145/1455770.1455786openalex-snapshot

Computational soundness of observational equivalence

inferredcites →https://doi.org/10.1145/1455770.1455817openalex-snapshot

Towards automated proofs for asymmetric encryption schemes in the random oracle model

inferredcites →https://doi.org/10.1145/1480881.1480894openalex-snapshot

Formal certification of code-based cryptographic proofs

inferredcites →https://doi.org/10.1145/1653662.1653672openalex-snapshot

CoSP

inferredcites →https://doi.org/10.1145/168588.168596openalex-snapshot

Random oracles are practical

inferredcites →https://doi.org/10.1145/1866307.1866350openalex-snapshot

Computational indistinguishability logic

inferredcites →https://doi.org/10.1145/2046707.2046717openalex-snapshot

A composable computational soundness notion

inferredcites →https://doi.org/10.1145/948109.948140openalex-snapshot

A composable cryptographic library with nested operations

inferredcites →https://doi.org/10.1145/948109.948142openalex-snapshot

Security proofs for an efficient password-based key exchange

inferredcites →https://doi.org/10.14279/tuj.eceasst.23.316openalex-snapshot

Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS

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-642-36830-1_4openalex-snapshot

Proved Generation of Implementations from Computationally Secure Protocol Specifications

inferred← citeshttps://doi.org/10.1007/978-3-642-41227-1_4openalex-snapshot

CIL Security Proof for a Password-Based Key Exchange

inferred← citeshttps://doi.org/10.1049/2023/9399887openalex-snapshot

Kyber, Saber, and SK‐MLWR Lattice‐Based Key Encapsulation Mechanisms Model Checking with Maude

inferred← citeshttps://doi.org/10.1109/csf.2017.7openalex-snapshot

Symbolic and Computational Mechanized Verification of the ARINC823 Avionic 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/csf51468.2021.00014openalex-snapshot

Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem

inferred← citeshttps://doi.org/10.1109/csf61375.2024.00015openalex-snapshot

Dealing with Dynamic Key Compromise in Crypto Verif

inferred← citeshttps://doi.org/10.1109/csf61375.2024.00019openalex-snapshot

CV2EC: Getting the Best of Both Worlds

inferred← citeshttps://doi.org/10.20868/upm.thesis.42973openalex-snapshot

Automation and Modularity of Cryptographic Proofs in the Computational Model

inferred← citeshttps://doi.org/10.3233/jcs-150524openalex-snapshot

Proved generation of implementations from computationally secure protocol specifications

inferred← citeshttps://doi.org/10.51983/ajeat-2017.6.2.819openalex-snapshot

Integrity and Privacy through Authentication Key Exchange Protocols for Distributed Systems

inferred← citeshttps://doi.org/10.70675/0a92ac6cze781z4eb7z91dbzbcb2cabbe038openalex-snapshot

Formal verification for real-world cryptographic protocols and implementations

showing the first 12 of 13 · page through all 13

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.