Abstract
This paper presents history-dependent scheduling, a new technique for reducing the search space in the verification of cryptographic protocols. This technique allows the detection of some “non-minimal” interleavings during a depth-first search, and was implemented in TRUST, our cryptographic protocol verifier. We give some experimental results showing that our method can greatly increase the efficiency of the verification procedure.
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
Amadio, R., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 380. Springer, Heidelberg (2000), Also RR-INRIA 3915
Amadio, R., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. RR-INRIA 4147 (March 2001); Revised version in Theoretical Computer Science 290(1), 695–740 (2003)
Basin, D., Mödersheim, S., Viganò, L.: Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. Technical Report 405, Dep. of Computer Science, ETH Zurich (2003)
Boreale, M.: Symbolic Trace Analysis of Cryptographic Protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 667. Springer, Heidelberg (2001)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. on Information Theory 29(2), 198–208 (1983)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)
Huima, A.: Efficient infinite-state analysis of security protocols. In: Proc. Formal methods and security protocols, FLOC Workshop, Trento (1999)
Lowe, G.: A hierarchy of authentication specifications. In: Proc. 10th IEEE Computer Security Foundations Workshop (1997)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. RR INRIA 4134 (March 2001)
Vanackère, V.: The TRUST protocol analyser, automatic and efficient verification of cryptographic protocols. In: VERIFY 2002 Workshop, Copenhagen (2002)
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
Vanackère, V. (2004). History-Dependent Scheduling for Cryptographic Processes. In: Steffen, B., Levi, G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2004. Lecture Notes in Computer Science, vol 2937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-24622-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20803-7
Online ISBN: 978-3-540-24622-0
eBook Packages: Springer Book Archive