Latex es un lenguaje de edición de documentos de alta calidad, especialmente orientado a la composición de libros, documentos científicos y técnicos que incluyen fórmulas o imágenes de alta calidad. Está compuesto por un conjunto de macros Tex (un lenguaje de bajo nivel) y se ha convertido casi en un estándar para publicaciones científicas en áreas como la matemática, física e ingeniería ya que se puede tener un control más fino sobre cualquier aspecto tipográfico del documento.

Security Protocol Animator (SPAN) es una herramienta libre de verificación para protocolos criptográficos que ayuda en la búsqueda y caracterización de ataques. La principal ventaja de esta aplicación es que permite usar diferentes técnicas de verificación a un mismo protocolo. Se puede decir que es una interfaz gráfica para el manejo de HLPSL (High-Level Protocol Specification Language) y CAS+ (una implementación del Protocolo de Autenticación Central), que permite la traducción entre estos lenguajes y además brinda una interfaz gráfica más amigable al usuario. SPAN ayuda a producir de manera interactiva secuencias de mensajes o MSC (Message Sequence Charts).

Esta herramienta se utiliza para la simulación de protocolo criptográficos, permite la simulación de intrusos de manera activa o pasiva, la construcción automática de ataques a los protocolos diseñados. La edición del protocolo se puede realiza mediante HLPSL o CAS+, teniendo la posibilidad de realizar conversiones entre dichos lenguajes. Algunas características de la interfaz gráfica se muestran en la Figura # 1.

Figura # 1: Descripción de la interfaz gráfica de SPAN.