Automatically Checking Commitment Protocols in ProVerif without False Attacks

  • Tom Chothia
  • Ben Smyth
  • Chris Staite
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9036)


ProVerif over-approximates the attacker’s power to enable verification of processes under replication. Unfortunately, this results in ProVerif finding false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. We introduce a method to reduce false attacks when analysing secrecy. First, we show how inserting phases into non-replicated processes enables a more accurate translation to Horn clauses which avoids some false attacks. Secondly, we generalise our methodology to processes under replication. Finally, we demonstrate the applicability of our technique by analysing BlueTooth Simple Pairing. Moreover, we propose a simplification of this protocol that achieves the same security goal.


Security Protocol Impersonation Attack Horn Clause Cryptographic Protocol Collision Attack 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the Pi Calculus. ACM Transactions on Information and System Security 10(3) (2007)Google Scholar
  2. 2.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 104–115. ACM Press (2001)Google Scholar
  3. 3.
    Allamigeon, X., Blanchet, B.: Reconstruction of Attacks against Cryptographic Protocols. In: CSFW 2005: 18th Computer Security Foundations Workshop, pp. 140–154. IEEE Computer Society (2005)Google Scholar
  4. 4.
    Arapinis, M., Cortier, V., Kremer, S., Ryan, M.: Practical everlasting privacy. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 21–40. Springer, Heidelberg (2013)Google Scholar
  5. 5.
    Backes, M., Hriţcu, C., Maffei, M.: Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus. In: CSF 2008: 21st IEEE Computer Security Foundations Symposium, pp. 195–209. IEEE Computer Society (2008)Google Scholar
  6. 6.
    Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. 12th ACM Conference on Computer and Communications Security (CCS 2005), pp. 16–25. ACM Press (2005)Google Scholar
  7. 7.
    Baudet, M.: Sécurité des protocoles cryptographiques: Aspects logiques et calculatoires. PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France (2007)Google Scholar
  8. 8.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE Computer Society (2001)Google Scholar
  9. 9.
    Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Blanchet, B.: Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security 17(4), 363–434 (2009)Google Scholar
  11. 11.
    Blanchet, B.: Private email communication (November 12, 2012)Google Scholar
  12. 12.
    Blanchet, B.: Security Protocol Verification: Symbolic and Computational Models. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 3–29. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  13. 13.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming 75(1), 3–51 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Blanchet, B., Cortier, V.: Private email communication (November 13, 2012)Google Scholar
  15. 15.
    Blanchet, B., Smyth, B.: ProVerif: Automatic Cryptographic Protocol Verifier User Manual & Tutorial (2011),
  16. 16.
    Blanchet, B., Smyth, B., Cheval, V.: Proverif 1.88: Automatic cryptographic protocol verifier, user manual and tutorial (2013)Google Scholar
  17. 17.
    Chang, R., Shmatikov, V.: Formal analysis of authentication in bluetooth device pairing. In: Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (2007)Google Scholar
  18. 18.
    Chen, L., Ryan, M.: Attack, Solution and Verification for Shared Authorisation Data in TCG TPM. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 201–216. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on tpm state registers. In: CSF 2011: 24th IEEE Computer Security Foundations Symposium, pp. 66–80. IEEE (2011)Google Scholar
  20. 20.
    Delaune, S., Ryan, M.D., Smyth, B.: Automatic verification of privacy properties in the applied pi-calculus. In: Karabulut, Y., Mitchell, J., Herrmann, P., Jensen, C.D. (eds.) IFIPTM 2008: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security. IFIP, vol. 263, pp. 263–278. Springer, Heidelberg (2008)Google Scholar
  21. 21.
    Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12(2), 247–311 (2004)Google Scholar
  22. 22.
    Bluetooth Special Interest Group. Specification of the bluetooth system (2001)Google Scholar
  23. 23.
    Bluetooth Special Interest Group. Simple pairing whitepaper (2006)Google Scholar
  24. 24.
    Breaking, G.L.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  25. 25.
    Meadows, C.: Open Issues in Formal Methods for Cryptographic Protocol Analysis. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds.) MMM-ACNS 2001. LNCS, vol. 2052, p. 21. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    Needham, R.M., Schroeder, M.D.: Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM 21(12), 993–999 (1978)CrossRefzbMATHGoogle Scholar
  27. 27.
    Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, ch. 6. IOS Press (2011)Google Scholar
  28. 28.
    Smyth, B., Ryan, M.D., Chen, L.: Formal analysis of privacy in Direct Anonymous Attestation schemes (2012)Google Scholar
  29. 29.
    Zhao, F., Hanatani, Y., Komano, Y., Smyth, B., Ito, S., Kambayashi, T.: Secure Authenticated Key Exchange with Revocation for Smart Grid. In: ISGT 2012: 3rd IEEE Power & Energy Society Conference on Innovative Smart Grid Technologies, pp. 1–8 (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Tom Chothia
    • 1
  • Ben Smyth
    • 2
  • Chris Staite
    • 1
  1. 1.School of Computer ScienceUniversity of BirminghamBirminghamUK
  2. 2.Mathematical and Algorithmic Sciences Lab, France Research CenterHuawei Technologies Co. Ltd.ParisFrance

Personalised recommendations