- Referenced in 95 articles
- Compiler for the Analysis of Security Protocols. Casper is a program that will take ... description of a security protocol in a simple, abstract language, and produce a CSP description...
- Referenced in 84 articles
- AVISPA (Automated Validation of Internet Security Protocols and Applications) is a push-button tool ... automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive ... formal language for specifying protocols and their security properties, and integrates diﬀerent back-ends that...
- Referenced in 72 articles
- variety of areas including robotics, security protocols, web-services, etc. For example, security specifications involving...
- Referenced in 78 articles
- performance, the protocol has been designed to achieve a remarkable list of security properties ... whether the protocol can be proven secure in a rigorous model of key-exchange security ... this question we analyze the MQV protocol in the Canetti-Krawczyk model of key exchange ... original protocol but for which all the MQV’s security goals can be formally proved...
- Referenced in 59 articles
- universally composable secure channel based on the KEM-DEM framework. For ISO standards on public ... paper investigates a more general hybrid protocol, secure channel, using KEM and DEM, such that...
- Referenced in 50 articles
- attention. We present a suite of security protocols optimized for sensor networks: SPINS. SPINS ... secure building blocks: SNEP and µTESLA. SNEP includes: data conﬁdentiality, two-party data authentication ... resource-constrained environments. We implemented the above protocols, and show that they are practical even...
- Referenced in 27 articles
- model checker for symbolic analysis of security protocols. We introduce the open-source fixed-point ... model checker OFMC for symbolic security protocol analysis, which extends the on-the-fly model ... automatically translated to IF.par OFMC performs both protocol falsification and bounded session verification by exploring ... Moreover, OFMC allows one to analyze security protocols with respect to an algebraic theory...
- Referenced in 69 articles
- Lauter and Mityagin recently presented a strong security definition for authenticated key agreement strengthening ... also described a protocol, called NAXOS, that enjoys a simple security proof ... pass protocol. On the other hand MQV does not have a security proof ... security proof is extremely complicated. This paper proposes a new authenticated key agreement protocol, called...
- Referenced in 16 articles
- tool: verification, falsification, and analysis of security protocols. With the rise of the Internet ... open networks, a large number of security protocols have been developed and deployed in order ... secure communication. The analysis of such security protocols has turned out to be extremely difficult ... research in formal analysis of security protocols. Unfortunately, there are no effective approaches...
- Referenced in 17 articles
- Existing cryptographic compilers can automatically generate secure computation protocols from high-level specifications ... executing, benchmarking, and comparing, efficient secure two-party computation protocols. TASTY is a new compiler ... compiler. We use TASTY to compare protocols for secure multiplication based on homomorphic encryption with ... TASTY allows to automatically generate efficient secure protocols for many privacy-preserving applications where...
- Referenced in 52 articles
- v2/v3) and Transport Layer Security (TLS v1) protocols as well as a full-strength general...
- Referenced in 38 articles
- CMQV Ustaoglu presents a secure and efficient key exchange protocol named CMQV, based ... NAXOS. Compared with the latter two protocols, on the one hand, CMQV achieves higher performance ... model to be as secure as NAXOS. However, CMQV enjoys the security proof under...
- Referenced in 14 articles
- prover for the symbolic analysis of security protocols. The Tamarin prover supports the automated, unbounded ... symbolic analysis of security protocols. It features expressive languages for specifying protocols, adversary models...
- Referenced in 20 articles
- role as a building block for security protocols. In this paper, we describe...
- Referenced in 19 articles
- step in many formal analyses of security protocols. In the framework of the applied...
- Referenced in 29 articles
- system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different ... formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more ... that failure to find attacks still guarantees security. In this paper we describe some state...
- Referenced in 14 articles
- machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language...
- Referenced in 13 articles
- tool for checking trace equivalence of security protocols. It works in the so-called symbolic ... model, representing protocols by processes in the applied pi-calculus, and allowing the user ... describe various security primitives by an equational theory. In order to show that two processes...
- Referenced in 8 articles
- Based Model Checker for Security Protocols. We present SATMC (SAT-based Model Checker), an open ... based bounded model checking  of security protocols. Under the standard assumptions of perfect cryptography...
- Referenced in 11 articles
- Interrogator model. The Interrogator is a protocol security analysis tool implemented in Prolog and based ... capability has a simple interface to the protocol and threat model...