References:

[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.