Abstract
Induction-guided falsification (IGF) is a combination of bounded model checking (BMC) and structural induction, which can be used for falsification of invariants. IGF can also be regarded as a combination of forward and backward reachability analysis methods. This is because BMC is a forward reachability analysis method and structural induction can be regarded as a backward reachability analysis method. We report on a case study in which a variant of IGF has been used to systematically find a counterexample showing that NSPK does not enjoy the agreement property.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Jackson, D.: Alloy: A lightweight object modeling notation. ACM TOSEM 11, 256–290 (2002)
Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyser and its meta-logical properties. TCS 367, 162–202 (2006)
Ogata, K., Nakano, M., Kong, W., Futatsugi, K.: Induction-guided falsification. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 114–131. Springer, Heidelberg (2006)
Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. CACM 21, 993–999 (1978)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Denker, G., Meseguer, J., Talcott, C.: Protocol specification and analysis in Maude. In: Workshop on Formal Methods and Security Protocols (1998)
Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS/CafeOBJ method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 596–615. Springer, Heidelberg (2006)
Gâinâ, D., Futatsugi, K., Ogata, K.: Constructor-based institutions. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 398–412. Springer, Heidelberg (2009)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE TIT IT-29, 198–208 (1983)
Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. IPL 56, 131–133 (1995)
de Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: CAV 2003. LNCS, vol. 2392, pp. 14–26. Springer, Heidelberg (2003)
de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
Zhang, M., Ogata, K., Nakamura, M.: Specification translation of state machines from equational theories into rewrite theories. In: Zhu, H. (ed.) ICFEM 2010. LNCS, vol. 6447, pp. 678–693. Springer, Heidelberg (2010)
Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Crème: An automatic invariant prover of behavioral specifications. IJSEKE 17, 783–804 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ogata, K., Futatsugi, K. (2010). A Combination of Forward and Backward Reachability Analysis Methods. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-16901-4_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16900-7
Online ISBN: 978-3-642-16901-4
eBook Packages: Computer ScienceComputer Science (R0)