• AGVI

  • Referenced in 4 articles [sw02287]
  • verification, and implementation of security protocols. As new Internet applications emerge, new security protocols ... designed and implemented. Unfortunately the current protocol design and implementation process is often ... toolkit AGVI, Automatic Generation, Verification, and Implementation of Security Protocols. With AGVI, the protocol designer ... cryptographic key setup) and security requirements. AGVI will then automatically find the near-optimal protocols...
  • LDYIS

  • Referenced in 3 articles [sw01359]
  • present a formalism for the automatic verification of security protocols based on multi-agent systems...
  • HERMES

  • Referenced in 9 articles [sw00403]
  • HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. Cryptography is not sufficient ... implementing secure exchange of secrets or authentification. Logical flaws in the protocol design may lead ... assumption of perfect cryptography. Most of protocol verification tools are model-checking tools for bounded ... applied to discover flaws in cryptographic protocols. On the contrary, tools based on induction...
  • SeVe

  • Referenced in 2 articles [sw06547]
  • SeVe: automatic tool for verification of security protocols Security protocols play more and more important ... introduced under this framework, and the verification algorithms are also given. The results of this ... which supports specifying, simulating, and verifying security protocols. The experimental results show that a SeVe ... types of security protocols and complements the state-of-the-art security verifiers in several...
  • OFMC

  • Referenced in 26 articles [sw09466]
  • point model checker OFMC for symbolic security protocol analysis, which extends ... protocol goals. AnB specifications are automatically translated to IF.par OFMC performs both protocol falsification ... bounded session verification by exploring, in a demand-driven way, the transition system resulting from ... reduction. Moreover, OFMC allows one to analyze security protocols with respect to an algebraic theory...
  • SPY

  • Referenced in 6 articles [sw22152]
  • global protocols, and their run-time verification through automatically generated, distributed endpoint monitors. Building ... validates communication safety properties on the global protocol, but enforces them via independent monitoring ... conform to the protocol. The global protocol specifications can be additionally elaborated to express finer ... security policies, supported by third-party plugins. Our demonstration use case is the verification...
  • SANDLog

  • Referenced in 2 articles [sw13794]
  • specification language for secure routing protocols for verifying properties of these protocols. We prove invariant ... towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof obligations ... generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols...
  • VCGen

  • Referenced in 2 articles [sw13795]
  • specification language for secure routing protocols for verifying properties of these protocols. We prove invariant ... towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof obligations ... generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols...
  • ASPIER

  • Referenced in 6 articles [sw09852]
  • standard protocol security model to automatically analyze authentication and secrecy properties of protocol implementations ... software model checking with a domain-specific protocol and symbolic attacker model. We have implemented ... part of an industrial strength protocol implementation - the handshake in OpenSSL - for configurations consisting ... evaluated them in the context of OpenSSL verification. ASPIER detected the ”version-rollback” vulnerability...
  • verifier

  • Referenced in 2 articles [sw12878]
  • verification of security proofs of quantum cryptographic protocols. We simplify the syntax and operational semantics ... quantum process calculus qCCS so that verification of weak bisimilarity of configurations becomes easier ... applied to the verification of Shor and Preskill’s unconditional security proof of BB84 ... unconditional security proof of BB84 against an unlimited adversary’s attack semi-automatically...
  • ACL2

  • Referenced in 275 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1758 articles [sw00161]
  • Coq is a formal proof management system. It...
  • gmp

  • Referenced in 260 articles [sw00363]
  • GMP is a free library for arbitrary precision...
  • Isabelle

  • Referenced in 601 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • jETI

  • Referenced in 15 articles [sw00471]
  • We present jETI, a redesign of the Electronic...
  • Magma

  • Referenced in 2747 articles [sw00540]
  • Computer algebra system (CAS). Magma is a large...
  • MapReduce

  • Referenced in 240 articles [sw00546]
  • MapReduce is a new parallel programming model initially...
  • Mathematica

  • Referenced in 5756 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • Matlab

  • Referenced in 11649 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • Nitpick

  • Referenced in 57 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that...