Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Secrecy and group creation
Cardelli L., Ghelli G., Gordon A. Information and Computation196 (2):127-155,2005.Type:Article
Date Reviewed: Aug 2 2005

Type systems for the pi-calculus have gained interest over the last few years as a framework for the analysis of security protocols. In this paper, the authors develop an extended, typed pi-calculus based on the notion of a group. Under this new approach, each name belongs to a group, which may be created dynamically by a creation operator. In this context, the type system prevents information leaks (secrets).

The authors devote significant effort to studying the secrecy properties derived from the notion of a group. As in some other contributions to this area, one of the key results of the paper is a theorem that guarantees the secrecy of names. In this case, however, the secrecy is relative to an “untyped” opponent, which is a strong result.

In the conclusion, the authors present some brief notes on related work. The apparent connection between the groups introduced in this work and the channels and binders used in control flow analysis as presented in Bodei et al. [1] is explicitly mentioned. Despite the differences that exist, I suspect that both approaches could benefit from a deeper study of these connections. In fact, some other works have also established very interesting relationships between typed process calculus and other systems [2].

Reviewer:  Juan Estevez-Tapiador Review #: CR131611 (0602-0182)
1) Bodei, C; Degano, P; Nielson, H; Riis Nielson, H Concurrency theory (CONCUR’98)LNCS 1466: LNCS 1466. Springer, Berlin, Germany, 1998.
2) Abadi, M; Blanchet, B Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52, 1(2005), 102–146.
Bookmark and Share
 
Lambda Calculus And Related Systems (F.4.1 ... )
 
 
Code Breaking (E.3 ... )
 
 
Formal Models Of Communication (E.4 ... )
 
 
Data Encryption (E.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Lambda Calculus And Related Systems": Date
Polymorphic rewriting conserves algebraic strong normalization
Breazu-Tannen V., Gallier J. Theoretical Computer Science 83(1): 3-28, 1991. Type: Article
Aug 1 1992
Metacircularity in the polymorphic &lgr;-calculus
Pfenning F. (ed), Lee P. (ed) Theoretical Computer Science 89(1): 137-159, 1991. Type: Article
Nov 1 1992
Quantitative domains and infinitary algebras
Lamarche F. Theoretical Computer Science 94(1): 37-62, 1992. Type: Article
Dec 1 1992
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