[1] Internet systems consortium. http://www.isc.org/. [2] Wide mouth frog protocol. http://en.wikipedia.org/wiki/Wide_Mouth_ Frog_protocol. [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 http://www.avispa-project.org/publications.html. [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. 49 [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 Society. [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. ACM. [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. 50 [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/ en/US/docs/ios/solutions_docs/mobile_ip/mobil_ip.html#wp1030824. [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. 51 [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 progress. [24] Thomas Kernen and Steve Simlo. Automatic ip multicast without explicit tunnels. EBU TECHNICAL REVIEW, 2010. [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 2005. [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 http://www.avispa-project.org/package/user-manual.pdf. 52 [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.