Abstract
Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be used for the verification of security protocols using a logic of belief. The underlying idea is to treat separately the temporal evolution and the belief aspects of principals. In practice, things work as follows: when we consider the temporal evolution of a principal we treat belief atoms (namely, atomic formulae expressing belief) as atomic propositions. When we deal with the beliefs of a principal A, we model its beliefs about another principal B as the fact that A has access to a representation of B as a process. Then, any time it needs to verify the truth value of some belief atom about B, e.g., B B ø, A simply tests whether, e.g., ø holds in its (appropriate) representation of B. Beliefs are essentially used to control the “jumping” among processes. Our approach allows us to reuse the technology and tools developed in model checking.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35533-7_26
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi and M. Tuttle. A semantics for a logic of authentication. In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, pages 201–216, 1991.
M. Benerecetti and F. Giunchiglia. Model checking security protocols using a logic of belief. In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000). March 27th - April 1st, 2000, Berlin, Germany. To appear.
M. Benerecetti, F. Giunchiglia, and L. Serafini. Model Checking Multiagent Systems. Journal of Logic and Computation, Special Issue on Computational & Logical Aspects of Multi-Agent Systems, 8 (3): 401–423, 1998.
M. Burrows, M. Abadi, and R. M. Needham. A logic of authentication. ACM Transactions on Computer Systems, 8 (1): 18–36, 1990.
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. Nusmv: a new symbolic model verifier. In Proceedings of the International Conference on Computer-Aided Verification (CAV’99) Trento, Italy. July 1999., 1999.
E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science Publisher B.V., 1990.
R. Fagin, J.Y. Halpem, Y. Moses, and M. Y. Vardi. Reasoning about knowledge. MIT Press, 1995.
W. Marrero, E.M. Clarke, and S. Jha. Model checking for security protocols. In DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.
J.C. Mitchell, M Mitchell, and U. Stem. Automated Analysis of Cryptographic Protocols Using Murphi. In IEEE Symp. Security and Privacy, pages 141–153, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Benerecetti, M., Giunchiglia, F., Panti, M., Spalazzi, L. (2000). A Logic of Belief and a Model Checking Algorithm for Security Protocols. In: Bolognesi, T., Latella, D. (eds) Formal Methods for Distributed System Development. PSTV FORTE 2000 2000. IFIP — The International Federation for Information Processing, vol 55. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35533-7_25
Download citation
DOI: https://doi.org/10.1007/978-0-387-35533-7_25
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5264-9
Online ISBN: 978-0-387-35533-7
eBook Packages: Springer Book Archive