Using SPIN to Detect Vulnerabilities in the AACS Drive-Host Authentication Protocol

  • Wei Wang
  • Dongyao Ji
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)


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].


AACS SPIN Model Checker LTL Authenticity Collusion Attack 


  1. 1.
    Intel et al. Advanced Access Content System (AACS) – Introduction and Common Cryptographic Elements. Revision 0.91, pp. 32–34 (2006)Google Scholar
  2. 2.
    Khan, A.S., Mukund, M., Suresh, S.P.: Generic Verification of Security Protocols. Technical Report, Chennai Mathematical Institute (2005)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Sui, J., Stinson, D.R.: A Critical Analysis and Improvement of AACS Drive-Host Authentication. Centre for Applied Cryptographic Research (CACR) (2007)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of computer security 6, 85–128 (1998)CrossRefGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. Journal of Computer Security 13(1), 135–165 (2005)CrossRefGoogle Scholar
  11. 11.
    Spin Workshop. Spin-Formal Verification (2008),

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Wei Wang
    • 1
  • Dongyao Ji
    • 1
  1. 1.The State Key Laboratory of Information SecurityGraduate University of Chinese Academy of ScienceBeijingP.R. China

Personalised recommendations