• EasyCrypt

  • Referenced in 33 articles [sw09738]
  • Computer-aided security proofs for the working cryptographer. We present EasyCrypt ... automated tool for elaborating security proofs of cryptographic systems from proof sketches-compact, 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 Cramer-Shoup...
  • 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 code-based 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...
  • zk-SNARK

  • Referenced in 13 articles [sw22495]
  • zero-knowledge 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 ... elliptic-curve 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]
  • Semi-automated verification of security proofs of quantum cryptographic protocols. This paper presents a formal ... semi-automated 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...
  • Maude-NPA

  • Referenced in 35 articles [sw12159]
  • system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different ... Maude-NPA. 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]
  • language-based system for efficient zero-knowledge 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 non-interactive zero-knowledge 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 Schnorr-type non-interactive zero ... knowledge proofs. Unlike zk-SNARKs, our techniques do not require trusted setup and only rely ... widely-used 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 proof-of-concept implementation...
  • WalnutDSA

  • Referenced in 5 articles [sw27489]
  • used as a basis for many different cryptographic applications. This one-way function was specifically ... security of the scheme, provides a proof of security under EUF-CMA, 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...