Automated Identification of Desynchronisation Attacks on Shared Secrets

  • Sjouke Mauw
  • Zach SmithEmail author
  • Jorge Toro-Pozo
  • Rolando Trujillo-Rasua
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11098)


Key-updating protocols are a class of communication protocol that aim to increase security by having the participants change encryption keys between protocol executions. However, such protocols can be vulnerable to desynchronisation attacks, a denial of service attack in which the agents are tricked into updating their keys improperly, impeding future communication. In this work we introduce a method that can be used to automatically verify (or falsify) resistance to desynchronisation attacks for a range of protocols. This approach is then used to identify previously unreported vulnerabilities in two published RFID grouping protocols.

Supplementary material


  1. 1.
    Abughazalah, S., Markantonakis, K., Mayes, K.: Two rounds RFID grouping-proof protocol. In: 2016 IEEE International Conference on RFID, RFID 2016, Orlando, FL, USA, 3–5 May 2016, pp. 161–174 (2016)Google Scholar
  2. 2.
    Avoine, G.: Adversarial model for radio frequency identification. IACR Cryptology ePrint Archive 2005, 49 (2005)Google Scholar
  3. 3.
    Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSF 2001, pp. 82–96 (2001)Google Scholar
  4. 4.
    Blanchet, B.: Using Horn clauses for analyzing security protocols. In: Formal Models and Techniques for Analyzing Security Protocols, vol. 5, pp. 86–111 (2011)Google Scholar
  5. 5.
    Cohn-Gordon, K., Cremers, C., Garratt, L.: On post-compromise security. In: CSF 2016, pp. 164–178. IEEE (2016)Google Scholar
  6. 6.
    van Deursen, T., Mauw, S., Radomirović, S., Vullers, P.: Secure ownership and ownership transfer in RFID systems. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 637–654. Springer, Heidelberg (2009). Scholar
  7. 7.
    van Deursen, T., Radomirovic, S.: Attacks on RFID protocols. IACR Cryptology ePrint Archive 2008, 310 (2008)Google Scholar
  8. 8.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Dreier, J., Duménil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equational theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117–140. Springer, Heidelberg (2017). Scholar
  10. 10.
    Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12(2), 247–311 (2004)CrossRefGoogle Scholar
  11. 11.
    Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217–273 (1992)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Juels, A.: “Yoking-proofs” for RFID tags. In: 2nd IEEE Conference on Pervasive Computing and Communications Workshops (PerCom 2004 Workshops), Orlando, FL, USA, 14–17 March 2004, pp. 138–143 (2004)Google Scholar
  13. 13.
    Jung, S.W., Jung, S.: HRP: A HMAC-based RFID mutual authentication protocol using PUF. In: International Conference on Information Networking (ICOIN), pp. 578–582. IEEE (2013)Google Scholar
  14. 14.
    Kapoor, G., Piramuthu, S.: Vulnerabilities in some recently proposed RFID ownership transfer protocols. In: First International Conference on Networks and Communications, pp. 354–357. IEEE (2009)Google Scholar
  15. 15.
    Li, Q.S., Xu, X.L., Chen, Z.: PUF-based RFID ownership transfer protocol in an open environment. In: 15th International Conference on Parallel and Distributed Computing, Applications and Technologies, pp. 131–137. IEEE (2014)Google Scholar
  16. 16.
    Li, T., Wang, G.: Security analysis of two ultra-lightweight RFID authentication protocols. In: Venter, H., Eloff, M., Labuschagne, L., Eloff, J., von Solms, R. (eds.) SEC 2007. IIFIP, vol. 232, pp. 109–120. Springer, Boston, MA (2007). Scholar
  17. 17.
    Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). Scholar
  18. 18.
    Peris-Lopez, P., Hernandez-Castro, J.C., Tapiador, J.M.E., Ribagorda, A.: Advances in ultralightweight cryptography for low-cost RFID tags: gossamer protocol. In: Chung, K.-I., Sohn, K., Yung, M. (eds.) WISA 2008. LNCS, vol. 5379, pp. 56–68. Springer, Heidelberg (2009). Scholar
  19. 19.
    Perrin, T., Marlinspike, M.: The double ratchet algorithm. GitHub Wiki (2016)Google Scholar
  20. 20.
    Radomirovic, S., Dashti, M.T.: Derailing attacks. In: Security Protocols XXIII - 23rd International Workshop, Cambridge, UK, 31 March- 2 April 2015, Revised Selected Papers, pp. 41–46 (2015)Google Scholar
  21. 21.
    Saito, J., Sakurai, K.: Grouping proof for RFID tags. In: 19th International Conference on Advanced Information Networking and Applications (AINA 2005), Taipei, Taiwan, 28–30 March 2005, pp. 621–624 (2005)Google Scholar
  22. 22.
    Srivastava, K., Awasthi, A.K., Kaul, S.D., Mittal, R.C.: A hash based mutual RFID tag authentication protocol in telecare medicine information system. J. Med. Syst. 39(1), 153 (2015)CrossRefGoogle Scholar
  23. 23.
    Sun, D., Zhong, J.: Cryptanalysis of a hash based mutual RFID tag authentication protocol. Wirel. Pers. Commun. 91(3), 1085–1093 (2016)CrossRefGoogle Scholar
  24. 24.
    Sundaresan, S., Doss, R., Piramuthu, S., Zhou, W.: A robust grouping proof protocol for RFID EPC C1G2 tags. IEEE Trans. Inf. Forensics Secur. 9(6), 961–975 (2014)CrossRefGoogle Scholar
  25. 25.
    Sundaresan, S., Doss, R., Zhou, W.: Secure ownership transfer in multi-tag/multi-owner passive RFID systems. In: Symposium on Selected Areas in Communications, Globecom 2013, pp. 2891–2896. IEEE (2013)Google Scholar
  26. 26.
    Sundaresan, S., Doss, R., Zhou, W.: Zero knowledge grouping proof protocol for RFID EPC C1G2 tags. IEEE Trans. Comput. 64(10), 2994–3008 (2015)MathSciNetCrossRefGoogle Scholar
  27. 27.
    The Tamarin Team: MS Windows NT Kernel Description (2018).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Sjouke Mauw
    • 1
    • 2
  • Zach Smith
    • 1
    Email author
  • Jorge Toro-Pozo
    • 1
  • Rolando Trujillo-Rasua
    • 2
    • 3
  1. 1.CSCUniversity of LuxembourgEsch-sur-AlzetteLuxembourg
  2. 2.SnTUniversity of LuxembourgEsch-sur-AlzetteLuxembourg
  3. 3.School of Information TechnologyDeakin UniversityGeelongAustralia

Personalised recommendations