Abstract
The inductive approach [1] has been successfully used for verifying a number of security protocols, uncovering hidden assumptions. Yet it requires a high level of skill to use: a user must guide the proof process, selecting the tactic to be applied, inventing a key lemma, etc. This paper suggests that a proof planning approach [2] can provide automation in the verification of security protocols using the inductive approach. Proof planning uses AI techniques to guide theorem provers. It has been successfully applied in formal methods to software development. Using inductive proof planning [3], we have written a method which takes advantage of the differences in term structure introduced by rule induction, a chief inference rule in the inductive approach. Using difference matching [4], our method first identifies the differences between a goal and the associated hypotheses. Then, using rippling [5], the method attempts to remove such differences. We have successfully conducted a number of experiments using HOL-Clam [6], a socket-based link that combines the HOL theorem prover [7] and the Clam proof planner [8]. While this paper key’s contribution centres around a new insight to structuring the proof of some security theorems, it also reports on the development of the inductive approach within the HOL system.
This research was partially supported by two grants: CONACYT 33337-A and ITESM CCEM-0302-05.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security 6, 85–128 (1998)
Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, R., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120X. Springer, Heidelberg (1988)
Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. Journal of Automated Reasoning 7, 303–324 (1991)
Basin, D., Walsh, T.: Difference unification. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence, IJCAI 1993, San Mateo, CA, vol. 1, pp. 116–122. Morgan Kaufmann, San Francisco (1993)
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence 62, 185–253 (1993)
Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between CLAM and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 87–104. Springer, Heidelberg (1998)
Gordon, M.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification. Kluwer, Dordrecht (1988)
Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 647–648. Springer, Heidelberg (1990)
Monroy, R., Bundy, A., Green, I.: Planning Proofs of Equations in CCS. Automated Software Engineering 7, 263–304 (2000)
Schneider, S.: Modelling Security Properties with CSP. Computer Science Department, Technical Report Series CSD-TR-96-04, Royal Holloway, University of London (1996)
Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 77–90. Academic Press, London (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
López, J.C., Monroy, R. (2004). A Rippling-Based Difference Reduction Technique to Automatically Prove Security Protocol Goals. In: Lemaître, C., Reyes, C.A., González, J.A. (eds) Advances in Artificial Intelligence – IBERAMIA 2004. IBERAMIA 2004. Lecture Notes in Computer Science(), vol 3315. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30498-2_37
Download citation
DOI: https://doi.org/10.1007/978-3-540-30498-2_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23806-5
Online ISBN: 978-3-540-30498-2
eBook Packages: Springer Book Archive