
EasyCrypt
 Referenced in 33 articles
[sw09738]
 Computeraided security proofs for the working cryptographer. We present EasyCrypt ... automated tool for elaborating security proofs of cryptographic systems from proof sketchescompact, formal representations ... theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool supports ... adoption by working cryptographers and illustrate its application to security proofs of the CramerShoup...

CertiCrypt
 Referenced in 6 articles
[sw09443]
 Programming language techniques for cryptographic proofs. CertiCrypt is a general framework to certify the security ... cryptographic primitives in the Coq proof assistant. CertiCrypt adopts the codebased paradigm, in which ... preserving program transformations) to assist in constructing proofs. Earlier publications of CertiCrypt provide an overview ... language techniques that arise specifically in cryptographic proofs. The techniques have been developed to complete...

zkSNARK
 Referenced in 13 articles
[sw22495]
 zeroknowledge proofs of knowledge for general NP statements are a powerful cryptographic primitive, both ... additional property, {it succinctness}, requiring the proof to be very short and easy to verify ... proofs: proving statements about acceptance of the proof system’s own verifier (and correctness ... ellipticcurve cryptographic techniques, and methods for exploiting the proof systems’ field structure and nondeterminism...

CoSP
 Referenced in 5 articles
[sw25389]
 symbolic models and for embedding these proofs into formal calculi. CoSP considers arbitrary equational theories ... proving x cryptographic primitives sound for y calculi only requires x + y proofs (instead ... conceptually decoupled from computational soundness proofs of cryptographic primitives. We exemplify the usefulness of CoSP...

verifier
 Referenced in 3 articles
[sw12878]
 Semiautomated verification of security proofs of quantum cryptographic protocols. This paper presents a formal ... semiautomated verification of security proofs of quantum cryptographic protocols. We simplify the syntax ... Shor and Preskill’s unconditional security proof of BB84. As a result, we succeed...

Geppetto
 Referenced in 10 articles
[sw31791]
 their results, but the overhead to produce proofs remains largely impractical. Geppetto introduces complementary techniques ... careful choice of cryptographic primitives, Geppetto’s instantiation of bounded proof bootstrapping improves on prior ... variety of source C programs and cryptographic libraries...

Timbuk
 Referenced in 47 articles
[sw06351]
 collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating ... instance, Timbuk is currently used to verify Cryptographic Protocols (see some papers...

Pinocchio
 Referenced in 42 articles
[sw10193]
 verifying general computations while relying only on cryptographic assumptions. With Pinocchio, the client creates ... uses the evaluation key to produce a proof of correctness. The proof is only...

HERMES
 Referenced in 9 articles
[sw00403]
 they are applied to discover flaws in cryptographic protocols. On the contrary, tools based ... induction and theorem proving provide a general proof strategy [9,4], but they are either...

libiop
 Referenced in 9 articles
[sw31793]
 rely only on lightweight symmetric cryptography (any cryptographic hash function). The library provides a tool ... chain for transforming certain types of probabilistic proofs (see below) into zkSNARKs with the above...

MaudeNPA
 Referenced in 35 articles
[sw12159]
 system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different ... MaudeNPA. We also provide completeness proofs, and experimental evaluations of their effect...

F*
 Referenced in 20 articles
[sw27563]
 tool with the expressive power of a proof assistant based on dependent types. After verification ... underlying cryptographic primitives. F*’s type system includes dependent types, monadic effects, refinement types ... combination of SMT solving and interactive proofs...

CryptHOL
 Referenced in 7 articles
[sw28582]
 CryptHOL provides a framework for formalising cryptographic arguments in Isabelle/HOL. It shallowly embeds a probabilistic ... generative probabilistic values, a codatatype. We derive proof rules for the operators and establish...

ZKPDL
 Referenced in 3 articles
[sw30793]
 languagebased system for efficient zeroknowledge proofs and electronic cash. In recent years, many ... processors. As a result, many advanced cryptographic protocols are now efficient enough to be considered ... language. ZKPDL implements noninteractive zeroknowledge proofs of knowledge, a primitive which has received ... have used our language to develop a cryptographic library, Cashlib, that provides an interface...

SCAPI
 Referenced in 3 articles
[sw22635]
 schemes belong to this layer). 3. Interactive cryptographic protocols: these are interactive protocols involving ... building blocks like commitment schemes, zero knowledge proofs and oblivious transfer. In addition, SCAPI includes...

zkledger
 Referenced in 1 article
[sw39963]
 balance sheet?” and gets a response and cryptographic assurance that the response is correct. zkLedger ... provides fast, rich auditing with a new proof scheme using Schnorrtype noninteractive zero ... knowledge proofs. Unlike zkSNARKs, our techniques do not require trusted setup and only rely ... widelyused cryptographic assumptions. Second, zkLedger provides completeness; it uses a columnar ledger construction...

CASPA_
 Referenced in 2 articles
[sw04078]
 automatically proving secrecy and authenticity properties of cryptographic protocols. The tool is grounded ... abstraction of protocol executions that allows establishing proofs of security for an unbounded number...

SAMBA
 Referenced in 1 article
[sw42123]
 also show that the overhead due to cryptographic primitives is linear in the size ... input, which is confirmed by our proofofconcept implementation...

WalnutDSA
 Referenced in 5 articles
[sw27489]
 used as a basis for many different cryptographic applications. This oneway function was specifically ... security of the scheme, provides a proof of security under EUFCMA, and discusses...

SPARKSkein
 Referenced in 1 article
[sw06871]
 reference implementation of the Skein cryptographic hash algorithm, written and verified using the SPARK language ... that it is subject to a proof of type safety. This proof also identified...