• Timbuk

  • Referenced in 46 articles [sw06351]
  • Timbuk is currently used to verify Cryptographic Protocols (see some papers and in the examples...
  • ProVerif

  • Referenced in 41 articles [sw06558]
  • ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev ... protocol by Horn clauses. Its main features are: It can handle many different cryptographic primitives ... unbounded number of sessions of the protocol (even in parallel) and an unbounded message space...
  • Design/CPN

  • Referenced in 37 articles [sw01952]
  • Modeling and verification of cryptographic protocols using coloured Petri nets and Design/CPN...
  • NRL

  • Referenced in 34 articles [sw12158]
  • protocol analyzer: An overview. The NRL protocol analyzer is a prototype special-purpose verification tool ... been developed for the analysis of cryptographic protocols that are used to authenticate principals...
  • Maude-NPA

  • Referenced in 29 articles [sw12159]
  • Maude-NRL protocol analyzer. The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool ... reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties...
  • Quark

  • Referenced in 20 articles [sw08447]
  • expressed by professionals, notably to implement cryptographic protocols in RFID technology. At the time...
  • TAPS

  • Referenced in 19 articles [sw02244]
  • TAPS: A first-order verifier for cryptographic protocols...
  • MCMAS-SLK

  • Referenced in 17 articles [sw24778]
  • results obtained for the dining cryptographers protocol and a variant of the cake-cutting problem...
  • VIFF

  • Referenced in 12 articles [sw05804]
  • computation is done using a cryptographic protocol which allows them to obtain a correct answer...
  • HERMES

  • Referenced in 9 articles [sw00403]
  • idealized assumption of perfect cryptography. Most of protocol verification tools are model-checking tools ... applied to discover flaws in cryptographic protocols. On the contrary, tools based on induction...
  • OFMC

  • Referenced in 27 articles [sw09466]
  • point model checker OFMC for symbolic security protocol analysis, which extends ... languages with support for algebraic properties of cryptographic operators and with a simple notation ... used both as assumptions and as protocol goals. AnB specifications are automatically translated to IF.par ... analyze security protocols with respect to an algebraic theory of the employed cryptographic operators, which...
  • CRAG

  • Referenced in 8 articles [sw06865]
  • Library provides an environment to test cryptographic protocols constructed from non-commutative groups, for example...
  • Spi2Java

  • Referenced in 5 articles [sw09935]
  • Spi2Java: automatic cryptographic protocol Java code generation from spi calculus. The aim of this work ... that automatically generates Java code implementing cryptographic protocols described in the formal specification language...
  • Apte

  • Referenced in 5 articles [sw20604]
  • website for the automatic cryptographic protocol verifier APTE: Algorithm for Proving Trace Equivalence. This tool ... Trace equivalence can be used to model cryptographic security properties such that privacy, anonymity, unlinkability...
  • DRNG

  • Referenced in 5 articles [sw15094]
  • generating high-quality keys for cryptographic protocols, and the RSEED instruction is provided for seeding...
  • Charm

  • Referenced in 10 articles [sw10192]
  • Charm, an extensible framework for rapidly prototyping cryptographic systems. Charm provides a number of features ... development of new protocols, including support for modular composition of cryptographic building blocks, infrastructure ... developing interactive protocols, and an extensive library of re-usable code. Our framework also provides ... cryptosystems to interoperate. We implemented over 40 cryptographic schemes using Charm, including some new ones...
  • Cryptyc

  • Referenced in 3 articles [sw12834]
  • Cryptyc: cryptographic protocol type checker. The Cryptyc system is a Cryptographic Protocol Type Checker. Unlike...
  • TASTY

  • Referenced in 17 articles [sw09865]
  • outcome. Existing cryptographic compilers can automatically generate secure computation protocols from high-level specifications...
  • verifier

  • Referenced in 2 articles [sw12878]
  • verification of security proofs of quantum cryptographic protocols. This paper presents a formal framework ... verification of security proofs of quantum cryptographic protocols. We simplify the syntax and operational semantics...
  • SCAPI

  • Referenced in 3 articles [sw22635]
  • implementing secure two-party and multiparty computation protocols (SCAPI stands for the “Secure Computation ... provides a reliable, efficient, and highly flexible cryptographic infrastructure. SCAPI is comprised of three layers ... belong to this layer). 3. Interactive cryptographic protocols: these are interactive protocols involving...