Abstract
In this paper we study abstraction techniques for verification problems of the form C ⊨ ϕ, where C is a first-order structure and ϕ is a first-order formula (both w.r.t. a given signature ∑). This study is motivated by the need of such abstractions for the automatic verification of properties of cryptographic protocols, which in our approach are modeled by first-order structures. Our so-called algebraic abstractions will be correct by construction and optimal in some certain technical sense. Moreover, we provide guidelines to design specific algebraic abstractions suited for verification problems corresponding to cryptographic protocols.
This work is partially supported by the RNTL project EVA funded by the French Ministry of Research.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. Astesiano, M. Broy, and G. Reggio. Algebraic specification of concurrent systems. chapter 13 in [2], pages 467–520, 1999.
E. Astesiano, H.-J. Kreowski, and B. Krieg-Brückner, editors. Algebraic Foundations of Systems Specification. Springer, 1999.
B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci and P. Schnoebelen. Systems and Software Verification. Springer, July 2001.
D. Bolignano. Towards a mechanization of cryptographic protocol verification. In Proc. 9th Int. Conf. Computer Aided Verification (CAV’97), Haifa, Israel, June 1997, volume 1254 of Lecture Notes in Computer Science, pages 131–142. Springer, 1997.
D. Bolignano. Using abstract interpretation for the safe verification of security protocols. In MFPS XV Mathematical Foundations of Programming Semantics, Fifteenth Conference, Tulane University, New Orleans, LA, April 28–May 1, 1999, volume 20 of Electronic Notes in Theor. Comp. Sci. Elsevier Science, 1999.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages (POPL’92), Albuquerque, New Mexico, January 19–22, 1992, pages 343–354. ACM Press, 1992.
Co.: The common framework initiative for algebraic specification and development. http://www.brics.dk/Projects/CoFI/.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2–3):103–179, 1992.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. In ACM Transactions on Programming Languages ans Systems, volume 19, 1997.
D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983.
J. Goubault-Larrecq. A method for automatic cryptographic protocol verification (extended abstract). In Proc. 15th IPDPS 2000 Workshops, Cancun, Mexico, May 2000, volume 1800 of Lecture Notes in Computer Science, pages 977–984. Springer, 2000.
S. Merz. Rules for abstraction. In R. K. Shyamasundar and K. Ueda, editors, Advances in Computing Science (ASIAN’97), volume 1345 of LNCS, pages 32–45, Berlin, Germany, 1997. Springer.
L. C. Paulson. The inductive approach to verifying cryptographic protocols. J. Computer Security, 6:85–128, 1998.
A. Tarlecki. Towards heterogeneous specifications. In Proc. Workshop on Frontiers of Combining Systems FroCoS’98,Amsterdam, October 1998, Applied Logic Series. Kluwer Academic Publishers, 1998. (To appear).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bidoit, M., Boisseau, A. (2002). Algebraic Abstractions. In: Cerioli, M., Reggio, G. (eds) Recent Trends in Algebraic Development Techniques. WADT 2001. Lecture Notes in Computer Science, vol 2267. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45645-7_2
Download citation
DOI: https://doi.org/10.1007/3-540-45645-7_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43159-6
Online ISBN: 978-3-540-45645-2
eBook Packages: Springer Book Archive