Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Verification methods for the computationally complete symbolic attacker based on indistinguishability
Bana G., Chadha R., Eeralla A., Okada M. ACM Transactions on Computational Logic21 (1):1-44,2019.Type:Article
Date Reviewed: Dec 16 2019

First-order logic formalization for security protocols and attackers enables formal verification. Once a formalization is established, standard tools such as a theorem prover can be used in the analysis.

Central to the formalization presented by the authors is a predicate for indistinguishability, that is, terms cannot be distinguished by a polynomial-time Turing machine with non-negligible probability. With the help of such a predicate, cryptographic properties such as the decisional Diffie-Hellman assumption can be axiomatized. The axioms are later translated into the language of the Coq theorem prover.

The authors build on their own previous work in first-order formalization, tackling multiple sessions in a protocol. To this end, they present and axiomatize an if_then_else statement.

The ideas are presented in detail and illustrated using the Diffie-Hellman key exchange. Because they focus the paper on extending their own previous work, the authors address readers from their particular field. The paper is not an ideal starting pointing for novices due to its heavy use of acronyms from the security field and many references to previous work.

Reviewer:  Andreas Schaefer Review #: CR146814 (2004-0078)
Bookmark and Share
 
Formal Methods (D.2.4 ... )
 
 
Verification (D.4.5 ... )
 
 
Security and Protection (D.4.6 )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
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