Abstract
Security protocols are crucial to achieve trusted computing. However, designing security protocols is not easy and so security protocols are typically faulty and have to be repaired. Continuing previous work we present first steps to automate this repairing process, especially for protocols that are susceptible to type-flaw attacks. To this end, we extend the notion of strand spaces by introducing an implementation layer for messages and extending the capabilities of a penetrator to swap messages that share the same implementation. Based on this framework we are able to track type flaw attacks to incompatibilities between the way messages are implemented and the design of concrete security protocols. Heuristics are given to either change the implementation or the protocol to avoid these situations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering 22(1), 6–15 (1996)
Anderson, R., Needham, R.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol. 963, pp. 236–247. Springer, Heidelberg (1995)
Aura, T.: Strategies against replay attacks. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop, CSFW 1997, pp. 59–69. IEEE Computer Society, Los Alamitos (1997)
Basin, D., Mödersheim, S., Viganò, L.: Algebraic intruder deductions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS, vol. 3835, pp. 549–564. Springer, Heidelberg (2005)
Basin, D.A., Mödersheim, S., Viganò, L.: Ofmc: A symbolic model checker for security protocols. International Journal of Information Security 4(3), 181–208 (2005)
Carlsen, U.: Cryptographic protocols flaws. In: Proceedings of the 7th IEEE Computer Security Foundations Workshop, CSFW 1994, pp. 192–200. IEEE Computer Society, Los Alamitos (1994)
Chevalier, Y., Rusinowitch, M.: Combining intruder theories. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 639–651. Springer, Heidelberg (2005)
Chevalier, Y., Vigneron, L.: Automated unbounded verification of security protocols. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 324–337. Springer, Heidelberg (2002)
Gao, H., Bodei, C., Degano, P.: A formal analysis of complex type flaw attacks on security protocols. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 167–183. Springer, Heidelberg (2008)
Guttman, J.-D., Thayer, F.-J.: Authentication tests and the structure of bundles. Theoretical Computer Science 283(2), 333–380 (2002)
Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW 2000, pp. 255–268. IEEE Computer Society, Los Alamitos (2000)
López-Pimentel, J.C., Monroy, R., Hutter, D.: On the automated correction of security protocols susceptible to a replay attack. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 594–609. Springer, Heidelberg (2007)
Malladi, S., Alves-Foss, J.: How to prevent type-flaw guessing attacks on password protocols. In: Proceedings of the 2003 Workshop on Foundations of Computer Security (FCS 2003), pp. 1–12. Technical Report of University of Ottawa (2003)
Malladi, S., Alves-Foss, J., Heckendorn, R.: On preventing replay attacks on security protocols. In: Proceedings of the International Conference on Security and Management, ICSM 2002, pp. 77–83 (2002), http://citeseer.ist.psu.edu/malladi02preventing.html (retrieved February 1, 2007)
Meadows, C.: Identifying potential type confusion in authenticated messages. In: Foundations of Computer Security 2002 (2002)
Meadows, C.: A procedure for verifying security against type confusion attacks. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop, CSFW 2003, pp. 62–74. IEEE Computer Society, Los Alamitos (2003)
Moore, J.H.: Protocol failures in cryptosystems. Proceedings of the IEEE 76(5), 594–602 (1988); reprinted in: Simmons, G.J. (ed.)Contemporary Cryptology: The Science of Information Integrity, pp. 541–558. IEEE Computer Science Press, Los Alamitos (1991)
Snekkenes, E.: Roles in cryptographic protocols. In: Proceedings of the 1992 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 105–119. IEEE Computer Society Press, Los Alamitos (1992)
Thayer, F.-J., Herzog, J.-C., Guttman, J.-D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2-3), 191–230 (1999)
Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Operating Systems Review 28(3), 24–37 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hutter, D., Monroy, R. (2009). On the Automated Correction of Protocols with Improper Message Encoding. In: Degano, P., Viganò, L. (eds) Foundations and Applications of Security Analysis. ARSPA-WITS 2009. Lecture Notes in Computer Science, vol 5511. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03459-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-03459-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03458-9
Online ISBN: 978-3-642-03459-6
eBook Packages: Computer ScienceComputer Science (R0)