• MOPS

  • Referenced in 23 articles [sw10117]
  • approach for finding bugs in security-relevant software and verifying their absence. The idea ... program to be verified as a pushdown automaton, represents the security property as a finite ... identify whether any state violating the desired security goal is reachable in the program ... approach are that it is sound in verifying the absence of certain classes of vulnerabilities...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • main ways to use UCLID: As a verifier, for term-level bounded model checking, correspondence ... design verification, analyzing software for security exploits, and verifying distributed algorithms...
  • F*

  • Referenced in 20 articles [sw27563]
  • code. This enables verifying the functional correctness and security of realistic applications. The main ongoing ... HTTPS stack in Project Everest. This includes verified implementations ... specifications for programs, including functional correctness and security properties. The F* type-checker aims...
  • ASPIER

  • Referenced in 6 articles [sw09852]
  • ASPIER: An Automated Framework for Verifying Security Protocol Implementations. We present ASPIER - the first framework ... software model checking with a standard protocol security model to automatically analyze authentication and secrecy ... ASPIER tool and used it to verify authentication and secrecy properties of a part...
  • SeVe

  • Referenced in 2 articles [sw06547]
  • many tools for specifying and verifying security protocols such as Casper/FDR, ProVerif, or AVISPA ... checker, which supports specifying, simulating, and verifying security protocols. The experimental results show that ... complements the state-of-the-art security verifiers in several aspects. Moreover, it also proves ... ability in building an automatic verifier for security protocols related to privacy type, which...
  • SANDLog

  • Referenced in 2 articles [sw13794]
  • program logic for verifying secure routing protocols. The Internet, as it stands today, is highly ... been done to understand and verify the formal security guarantees of proposed secure inter-domain ... declarative specification language for secure routing protocols for verifying properties of these protocols. We prove ... encoded several proposed secure routing mechanisms in SANDLog, verified variants of path authenticity properties...
  • VCGen

  • Referenced in 2 articles [sw13795]
  • program logic for verifying secure routing protocols. The Internet, as it stands today, is highly ... been done to understand and verify the formal security guarantees of proposed secure inter-domain ... declarative specification language for secure routing protocols for verifying properties of these protocols. We prove ... encoded several proposed secure routing mechanisms in SANDLog, verified variants of path authenticity properties...
  • KIV

  • Referenced in 53 articles [sw10060]
  • Karlsruhe Interactive Verifier (KIV). KIV is an interactive theorem prover with a user definable object ... Environment (VSE) developed for the German Information Security Agency. For this pursose, KIV was integrated...
  • maskVerif

  • Referenced in 2 articles [sw40780]
  • implement an automated approach for verifying security of masked implementations in presence of physical defaults...
  • Geppetto

  • Referenced in 10 articles [sw31791]
  • interest in Verifiable Computation protocols, which allow a weak client to securely outsource computations ... dramatically reduced the client’s cost to verify the correctness of their results...
  • EasyCrypt

  • Referenced in 33 articles [sw09738]
  • present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches ... automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool ... working cryptographers and illustrate its application to security proofs of the Cramer-Shoup and Hashed...
  • QUAIL

  • Referenced in 3 articles [sw19647]
  • arbitrary-precision quantitative analysis of the security of a system depending on private information. QUAIL ... depending on secret data, allowing to verify a security protocol’s effectiveness. We experiment with...
  • verifier

  • Referenced in 3 articles [sw12878]
  • addition, we generalize qCCS to handle security parameters and quantum states symbolically. We then prove ... proposed framework. A software tool, named the verifier, is implemented and applied to the verification ... unconditional security proof of BB84. As a result, we succeed in verifying the main part...
  • ConfigChecker

  • Referenced in 1 article [sw28842]
  • ConfigChecker: A tool for comprehensive security configuration analytics. Recent studies show that configurations of network ... packet in the network and verify network reachability and security requirements. Thus, our contributions ... configurations that allows for general reachability and security property-based verification using CTL model checking ... comprehensive analysis queries in order to verify security and risk requirements across...
  • JavaSPI

  • Referenced in 3 articles [sw23647]
  • framework, where the user can write a security protocol symbolic model in Java, using ... symbolically executed in the Java debugger, formally verified with ProVerif, and further refined ... that, for the usual security properties, a property verified by ProVerif on the symbolic model...
  • TulaFale

  • Referenced in 14 articles [sw00986]
  • complementary machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language ... then runs Blanchet’s resolution-based protocol verifier. Hence, we can automatically verify authentication properties...
  • CoCon

  • Referenced in 1 article [sw40174]
  • present a case study in formally verified security for realistic systems: the information flow security ... Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary ... expressiveness have led to bounded-deducibility security, a novel security model and verification method generally...
  • JPAC

  • Referenced in 1 article [sw19151]
  • formalisms used in concert can provide verifiably secure programming systems for Internet applications...
  • SPVT-II

  • Referenced in 2 articles [sw02728]
  • SPVT-II: An efficient security protocol verifier based on logic programming...
  • ComFoRT

  • Referenced in 10 articles [sw07533]
  • security requirements. In ComFoRT, these requirements are encoded as behavioral assertions that are verified automatically...