Abstract
In this paper, we use SPIN, a model checker for LTL, to detect vulnerabilities in the AACS drive-host authentication protocol. Before the detection, we propose a variant of the Dolev-Yao attacker model [4] and incorporate the synthesis and analysis rules [7] to formalize the protocol and the intruder capabilities. During the detection, we check the authenticity of the protocol and identify a few weaknesses. Besides, we propose a novel collusion attack that seriously threaten the security of the protocol, and build a corresponding LTL formula. Based on the formula, SPIN detects a few relevant attack instances in the original scheme of the authentication protocol and a modified scheme advanced in [5].
Keywords
Download to read the full chapter text
Chapter PDF
References
Intel et al. Advanced Access Content System (AACS) – Introduction and Common Cryptographic Elements. Revision 0.91, pp. 32–34 (2006)
Khan, A.S., Mukund, M., Suresh, S.P.: Generic Verification of Security Protocols. Technical Report, Chennai Mathematical Institute (2005)
Basin, D., Mödersheim, S., Viganó, L.: An On-the-fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Sui, J., Stinson, D.R.: A Critical Analysis and Improvement of AACS Drive-Host Authentication. Centre for Applied Cryptographic Research (CACR) (2007)
Henry, K., Sui, J., Zhong, G.: An Overview of the Advanced Access Content System (AACS). Centre for Applied Cryptographic Research (CACR), 2007 April 12 (2007)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of computer security 6, 85–128 (1998)
Maggi, P., Sisto, R.: Using SPIN to Verify Security Properties of Cryptographic Protocols. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 187–204. Springer, Heidelberg (2002)
Ramanujam, R., Suresh, S.P.: A decidable subclass of unbounded security protocols. In: Proc. IFIP Workshop on Issues in the Theory of Security (WITS–3), Warsaw (Poland), pp. 11–20 (2003)
Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. Journal of Computer Security 13(1), 135–165 (2005)
Spin Workshop. Spin-Formal Verification (2008), http://spinroot.com/spin/whatispin.html
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wang, W., Ji, D. (2008). Using SPIN to Detect Vulnerabilities in the AACS Drive-Host Authentication Protocol. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2008. FORTE 2008. Lecture Notes in Computer Science, vol 5048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68855-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-68855-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68854-9
Online ISBN: 978-3-540-68855-6
eBook Packages: Computer ScienceComputer Science (R0)