Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Analyzing security protocols with secrecy types and logic programs
Abadi M., Blanchet B. Journal of the ACM52 (1):102-146,2005.Type:Article
Date Reviewed: Mar 18 2005

This paper extends previous efforts carried out by Abadi and Blanchet toward the use of type systems to analyze security protocols. Some classic work on information flow security relies on assigning security classes to objects. A crucial point is to guarantee that no information may flow from higher to lower classes, thus preventing security leakages. The underlying idea here is somewhat similar, though the notion of a security class is formalized as a “type,” much in the same way that type is formalized in a programming language. From a security point of view, useful types are “public,” “secret,” and “any.” Each object--a key, a communication channel, or any other piece of information--is assigned a type, and rules of composability are provided for typing a complex object composed of simpler units of data. At the core of this approach, there is a general type system for a process algebra that extends the classic pi calculus. It is supported by a main theorem that states that well-typed processes preserve the secrecy of any value of level “any,” namely, they do not reveal secrets.

This work is, in my opinion, a sound contribution to the field. Nevertheless, I find the second part of the paper even more revealing, where the authors establish a connection between typed process calculus and a completely different approach: logic programs. Traditionally, logic schemes rely on a symbolic analysis that has been fully disconnected from the process calculus approach. The authors prove the equivalence of both approaches, a result of great interest.

To the best of my knowledge, this is one of the few works that tries to explore the relationships among the different frameworks for specifying and reasoning about security properties in protocols. I think understanding these relationships may be highly useful, for example, in interpreting the implications of the important results of one system on another.

Reviewer:  Juan Estevez-Tapiador Review #: CR131008 (0507-0792)
Bookmark and Share
  Reviewer Selected
 
 
Security and Protection (C.2.0 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Mechanical Verification (F.3.1 ... )
 
 
Process Models (F.3.2 ... )
 
 
Protocol Verification (C.2.2 ... )
 
 
Network Protocols (C.2.2 )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Security and Protection": Date
Introduction to data security and controls (2nd ed.)
Edward R. I., QED Information Sciences, Inc., Wellesley, MA, 1991. Type: Book (9780894353864)
Aug 1 1992
Security for computer networks: an introduction to data security in teleprocessing and electronic funds transfer
Davies D., Price W., John Wiley & Sons, Inc., New York, NY, 1984. Type: Book (9780471900634)
Oct 1 1985
The development and proof of a formal specification for a multilevel secure system
Glasgow J., Macewen G. ACM Transactions on Computer Systems 5(2): 151-184, 1987. Type: Article
Oct 1 1987
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