Abstract
We present a generic algorithm for solving Horn clauses through iterative specialisation. The algorithm is generic in the sense that it can be instantiated with any decidable fragment of Horn clauses, resulting in a solution scheme for general Horn clauses that guarantees soundness and termination, and furthermore, it presents sufficient criteria for completeness. We then demonstrate the use of the framework, by creating an instance of it, based on the decidable class \({\mathcal{H}_1}\), capable of solving a non-trivial protocol analysis problem based on the Yahalom protocol.
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
Tärnlund, S.Å.: Horn clause computability. BIT 17(2), 215–226 (1977)
van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733–742 (1976)
Nielson, F., Nielson, H.R., Seidl, H.: Normalizable horn clauses, strongly recognizable relations, and spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)
Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real c code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005)
Goubault-Larrecq, J.: Deciding h \(_{\mbox{1}}\) by resolution. Inf. Process. Lett. 95(3), 401–408 (2005)
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)
Paulson, L.C.: Relations between secrets: Two formal analyses of the yahalom protocol. Journal of Computer Security 9(3), 197–216 (2001)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. Journal of Computer Security 13(3), 347–390 (2005)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society, Los Alamitos (2001)
Seidl, H., Verma, K.N.: Cryptographic protocol verification using tractable classes of horn clauses. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 97–119. Springer, Heidelberg (2007)
Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Nielson, F., Nielson, H.R., Hansen, R.R.: Validating firewalls using flow logics. Theor. Comput. Sci. 283(2), 381–418 (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rosenkilde Nielsen, C., Nielson, F., Riis Nielson, H. (2008). Iterative Specialisation of Horn Clauses. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)