Login | Register

Formal Validation of Security Properties of AMT's Three-Way Handshake


Formal Validation of Security Properties of AMT's Three-Way Handshake

Salem, Ali Mohamad (2011) Formal Validation of Security Properties of AMT's Three-Way Handshake. Masters thesis, Concordia University.

PDF - Accepted Version


Multicasting is a technique for transmitting the same information to multiple receivers over IP networks. It is often deployed on streaming media applications over the
Internet and private networks. The biggest problem multicast introduces today is that it is an all or nothing solution. Every element on the path between the source and the receivers (links, routers, firewalls) requires multicast protocols to be enabled. Furthermore, multicast has a conceptual business model, and therefore is not an easy case to make. These factors, embedded deep in technology, but ultimately shaped by economics, led to a lack of multicast deployment. To address this problem, the AMT (Automatic IP Multicast without explicit Tunnels) specification has been
developed by the Network Working Group at the IETF. This specification is designed to provide a mechanism for a migration path to a fully multicast-enabled backbone.
It allows multicast to reach unicast-only receivers without the need for any explicit tunnels between the receiver and the source. We have formally validated the three-way
handshake in the AMT specification using AVISPA against two main security goals: secrecy and authentication. We have demonstrated that the authentication goal is not met: an attacker can masquerade as an AMT relay, and the AMT gateway (at the end user) cannot distinguish a valid relay from an invalid one. Another attack was also found where an intruder can disconnect or shutdown a valid session for a valid end-user using a replay attack.

Divisions:Concordia University > Faculty of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (Masters)
Authors:Salem, Ali Mohamad
Institution:Concordia University
Degree Name:M. Comp. Sc.
Program:Computer Science
Date:15 April 2011
Thesis Supervisor(s):Atwood, Bill
Keywords:Automatic IP Multicast without Explicit Tunnels, AMT, Multicast, Formal Validation, AVISPA, HLPSL, three-way handshake
ID Code:7324
Deposited By: ALI SALEM
Deposited On:09 Jun 2011 19:36
Last Modified:10 Jan 2012 13:30
[1] Internet systems consortium. http://www.isc.org/.
[2] Wide mouth frog protocol. http://en.wikipedia.org/wiki/Wide_Mouth_
[3] Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca
Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille He�am, Jacopo
Mantovani, Sebastian M�odersheim, David von Oheimb, Micha�el Rusinowitch,
Judson Santiago, Mathieu Turuani, Luca Vigan�o, and Laurent Vigneron.
The AVISPA Tool for the Automated Validation of Internet Security
Protocols and Applications. In Kousha Etessami and Sriram K. Rajamani,
editors, Proceedings of the 17th International Conference on Computer Aided
Veri�cation (CAV'05), volume 3576 of LNCS. Springer, 2005. Available at
[4] Alessandro Armando, David A. Basin, Mehdi Bouallagui, Yannick Chevalier,
Luca Compagna, Sebastian M�odersheim, Micha�el Rusinowitch, Mathieu Turuani,
Luca Vigan�o, and Laurent Vigneron. The aviss security protocol analysis
tool. In Proceedings of the 14th International Conference on Computer Aided
Veri�cation, CAV '02, pages 349{353, London, UK, UK, 2002. Springer-Verlag.
[5] Alessandro Armando and Luca Compagna. Sat-based model-checking for security
protocols analysis. Int. J. Inf. Secur., 7:3{32, January 2008.
[6] Joe Salowey Hao Zhou Glen Zorn S. Josefsson Ashwin Palekar, Dan Simon. Protected
EAP Protocol (PEAP) Version 2. Internet-Draft draft-josefsson-pppexteap-
tls-eap-10, Internet Engineering Task Force, October 2004. Work in progress.
[7] Stylianos Basagiannis, Panagiotis Katsaros, and Andrew Pombortsis. An intruder
model with message inspection for model checking security protocols.
Computers Security, 29(1):16{34, 2010.
[8] B. Blanchet and A. Chaudhuri. Automated formal analysis of a protocol for
secure �le sharing on untrusted storage. In Security and Privacy, 2008. SP
2008. IEEE Symposium on, pages 417 {431, May 2008.
[9] Bruno Blanchet. An E�cient Cryptographic Protocol Veri�er Based on Prolog
Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14),
pages 82{96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer
[10] Yohan Boichut, Pierre-Cyrille H�eam, Olga Kouchnarenko, and F. Oehl. Improvements
on the Genet and Klay technique to automatically verify security
protocols. In Proc. Int. Ws. on Automated Veri�cation of In�nite-State Systems
(AVIS'2004), joint to ETAPS'04, pages 1{11, Barcelona, Spain, April 2004. The
�nal version will be published in EN in Theoretical Computer Science, Elsevier.
[11] Jan Cederquist and Mohammad Torabi Dashti. An intruder model for verifying
liveness in security protocols. In Proceedings of the fourth ACM workshop on
Formal methods in security, FMSE '06, pages 23{32, New York, NY, USA, 2006.
[12] Iliano Cervesato. The dolev-yao intruder is the most powerful attacker. In
Proceedings of the Sixteenth Annual Symposium on Logic in Computer Science
| LICS'01, pages 16{19. IEEE Computer Society Press. Short, 2001.
[13] Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, J. Mantovani,
S. M�odersheim, and L. Vigneron. A high level protocol speci�cation language
for industrial security-sensitive protocols. In Austrian Computer Society, pages
193{205, 2004.
[14] Yannick Chevalier and Laurent Vigneron. Automated Unbounded Veri�cation
of Security Protocols. Research Report RR-4369, INRIA, 2002.
[15] Cisco. Introduction to mobile ip. 2001. Available at http://www.cisco.com/
[16] John Clark and Jeremy Jacob. A survey of authentication protocol literature.
Technical report, Carried out as part of a Strategic Research Plan managed by
Peter Ryan of the Defence Evaluation Research Agency, 1997.
[17] G. Denker and J. Millen. Capsl integrated protocol environment. In DARPA
Information Survivability Conference and Exposition, 2000. DISCEX '00. Pro-
ceedings, 2000.
[18] D. Dolev and A. Yao. On the security of public key protocols. Information
Theory, IEEE Transactions on, 29(2):198 { 208, March 1983.
[19] Bill Fenner, Mark Handley, Hugh Holbrook, and Isidor Kouvelas. Protocol Independent
Multicast - Sparse Mode (PIM-SM): Protocol Speci�cation (Revised).
RFC 4601, IETF, August 2006.
[20] Leonard A. Giuliano. Next generation tv over the internet: This revolution will
be televised. Technical report, 2011.
[21] Lawrence Harte. Introduction to Data Multicasting, IP Multicast Streaming for
Audio and Video Media Distribution. Althos, 2008.
[22] M. Hussain and D. Seret. A comparative study of security protocols validation
tools: Hermes vs. avispa. In Advanced Communication Technology, 2006. ICACT
2006. The 8th International Conference, volume 1, pages 303{308, 2006.
[23] Charlie Kaufman. Internet Key Exchange (IKEv2) Protocol. Internet-Draft
draft-ietf-ipsec-ikev2-17, Internet Engineering Task Force, 2005. Work in
[24] Thomas Kernen and Steve Simlo. Automatic ip multicast without explicit tunnels.
[25] A Lomuscio and W Penczek. Ldyis: a framework for model checking security
protocols. Fundamenta Informaticae, 85(1-4):359{375, 2008.
[26] J.C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic
protocols using mur phi;. In Security and Privacy, 1997. Proceedings., 1997
IEEE Symposium on, pages 141 {151, May 1997.
[27] Juniper Networks. Video distribution in a hybrid multicastunicast world. Mar
[28] Simon Blake-Wilson Paul Funk. EAP Tunneled TLS Authentication Protocol
(EAP-TTLS). Internet-Draft draft-ietf-pppext-eap-ttls-05, Internet Engineering
Task Force, 2004. Work in progress.
[29] Dawn Xiaodong Song. Athena: a new e�cient automatic checker for security protocol
analysis. In Computer Security Foundations Workshop, 1999. Proceedings
of the 12th IEEE, 1999.
[30] The AVISPA Team. Avispa v1.1 user manual. page 0088, 2006. Available at
[31] D. Thaler, M. Talwar, A. Aggarwal, L. Vicisano, and T. Pusateri. Automatic IP
Multicast Without Explicit Tunnels (AMT). Internet-Draft draft-ietf-mbonedauto-
multicast-10, Internet Engineering Task Force, 2010. Work in progress.
[32] Luca Vigan�o. Automated security protocol analysis with the avispa tool. Elec-
tron. Notes Theor. Comput. Sci., 155:61{86, May 2006.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page


Downloads per month over past year

Back to top Back to top