Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Beyond subterm-convergent equational theories in automated verification of stateful protocols
Dreier J., Duménil C., Kremer S., Sasse R.  POST 2017 (Proceedings of the 6th International Conference on Principles of Security and Trust, Uppsala, Sweden, Apr 22-29, 2017)117-140.2017.Type:Proceedings
Date Reviewed: Oct 26 2017

The Tamarin Prover, a protocol analyzer tool for security protocols with cryptographic primitives, accepts protocols including cryptographic primitives such as encryption, signatures, and hash functions. More advanced primitives are also possible, such as Diffie–Hellman exponentiation, bilinear pairings, and multisets, but using a more elaborate implementation makes primitive combination more difficult. A more user-definable syntax for cryptographic primitives is also possible, but it uses subterm convergent equational theories, which can encode some primitives such as cancellation of encryption and decryption, but cannot encode other primitives such as exclusive-or, blind signatures, or trapdoor commitment. This paper provides new reasoning capabilities for the Tamarin Prover.

This paper represents a step forward in expanding the user-definable cryptographic primitives allowed by the Tamarin Prover by relying on equational theories satisfying the finite variant property, called finite variant theories. This class of theories can encode exclusive-or, blind signatures, or trapdoor commitment. However, the results in the paper are preliminary because not all of the finite variant theories are accepted. Those accepted are only a subset useful for encoding blind signatures or trapdoor commitment, but not exclusive-or.

Dreier et al. describe how both intruder reasoning and the normal dependency graphs of the Tamarin Prover are extended to the subclass of finite variant theories. Intruder reasoning uses K-up and K-down inference rules, whereas the normal dependency graphs use term simplification properties. The paper also provides several case studies, that is, protocols using cryptographic primitives encoded into the subclass of finite variant theories. It shows how several security properties, including secrecy, authentication, and indistinguishability, can be verified for those case studies.

This paper is useful to understand how the Tamarin Prover works and to understand how different cryptographic primitives are encoded into equational theories.

Reviewer:  Santiago Escobar Review #: CR145618 (1712-0811)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Verification (D.4.5 ... )
 
 
Cryptographic Controls (D.4.6 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Verification": Date
Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generator
Aharon A., Dorfman B., Gofman E., Leibowitz M., Schwartzburd V., Bar-David A. IBM Systems Journal 30(4): 527-538, 1991. Type: Article
Dec 1 1993
A Specification and Verification Method for Preventing Denial of Service
Yu C., Gligor V. IEEE Transactions on Software Engineering 16(6): 581-592, 1990. Type: Article
Feb 1 1991
Using program transformations to provide safety properties for real-time systems
Tsai G., Wang S. Real-Time Systems 27(2): 191-207, 2004. Type: Article
Feb 23 2005
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy