Non-collaborative Attackers and How and Where to Defend Flawed Security Protocols (Extended Version)

  • Michele Peroli
  • Luca ViganòEmail author
  • Matteo Zavatteri
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8809)


Security protocols are often found to be flawed after their deployment. We present an approach that aims at the neutralization or mitigation of the attacks to flawed protocols: it avoids the complete dismissal of the interested protocol and allows honest agents to continue to use it until a corrected version is released. Our approach is based on the knowledge of the network topology, which we model as a graph, and on the consequent possibility of creating an interference to an ongoing attack of a Dolev-Yao attacker, by means of non-collaboration actuated by ad-hoc benign attackers that play the role of network guardians. Such guardians, positioned in strategical points of the network, have the task of monitoring the messages in transit and discovering at runtime, through particular types of inference, whether an attack is ongoing, interrupting the run of the protocol in the positive case. We study not only how but also where we can attempt to defend flawed security protocols: we investigate the different network topologies that make security protocol defense feasible and illustrate our approach by means of concrete examples.


Security protocols Defense Non-collaborative attackers Attack interference Attack mitigation Topological advantage 


  1. 1.
    Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cuéllar, J., Erzse, G., Frau, S., Minea, M., Mödersheim, S., von Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Viganò, L.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Basin, D., Caleiro, C., Ramos, J., Viganò, L.: Distributed temporal logic for the analysis of security protocol models. Theor. Comput. Sci. 412(31), 4007–4043 (2011)CrossRefzbMATHGoogle Scholar
  3. 3.
    Bella, G.: A protocol’s life after attacks. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2003. LNCS, vol. 3364, pp. 11–18. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Bella, G., Bistarelli, S., Massacci, F.: Retaliation against protocol attacks. J. Inf. Assur. Secur. 3, 313–325 (2008)Google Scholar
  5. 5.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proceedings of CSF’01, pp. 82–96. IEEE CS Press (2001)Google Scholar
  6. 6.
    Boyd, C., Mathuria, A.: Protocols for Authentication and Key Establishment. Information Security and Cryptography. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Ciobâcǎ, S., Cortier, V.: Protocol composition for arbitrary primitives. In: Proceedings of CSF’10. IEEE CS Press (2010)Google Scholar
  8. 8.
    Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0 (1997)Google Scholar
  9. 9.
    Conti, M., Dragoni, N., Gottardo, S.: MITHYS: mind the hand you shake - protecting mobile devices from SSL usage vulnerabilities. In: Accorsi, R., Ranise, S. (eds.) STM 2013. LNCS, vol. 8203, pp. 65–81. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Cortier, V., Delaune, S.: Safely composing security protocols. Form. Methods Syst. Des. 34(1), 1–36 (2009)CrossRefzbMATHGoogle Scholar
  11. 11.
    Cremers, C.J.F.: The Scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198–208 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Fiazza, M.-C., Peroli, M., Viganò, L.: Attack interference: a path to defending security protocols. In: Obaidat, M.S., Sevillano, J.L., Filipe, J. (eds.) ICETE 2011. CCIS, vol. 314, pp. 296–314. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  15. 15.
    Fiazza, M.-C., Peroli, M., Vigano, L.: An environmental paradigm for defending security protocols. In: 2012 International Conference on Collaboration Technologies and Systems (CTS), May 2012, pp. 427–438 (2012)Google Scholar
  16. 16.
    ISO: ISO-IEC JTC1.27.02.2( entity authentication using symmetric techniques. International Organization for Standardization (ISO) (1990)Google Scholar
  17. 17.
    Mödersheim, S., Viganò, L.: Secure pseudonymous channels. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 337–354. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  18. 18.
    Peroli, M., Viganò, L., Zavatteri, M.: Non-collaborative Attackers and How and Where to Defend Flawed Security Protocols (Extended Version) (2014).
  19. 19.
    Ryan, P., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, B.: Modelling and Analysis of Security Protocols. Addison Wesley, Reading (2000)Google Scholar
  20. 20.
    Viganò, L.: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61–86 (2006)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Michele Peroli
    • 1
  • Luca Viganò
    • 2
    Email author
  • Matteo Zavatteri
    • 1
  1. 1.Dipartimento di InformaticaUniversità di VeronaVeronaItaly
  2. 2.Department of InformaticsKing’s College LondonLondonUK

Personalised recommendations