Latex is a language for high quality editing documents, especially oriented to book composition, scientific and technical documents, that include formulas and high quality images. It consists on a set of Tex macros (one low-level language) and has become almost a standard for scientific publications in areas such as mathematics, physics and engineering, since we can have finer control over any typographical appearance of the document.

Security Protocol Animator (SPAN) is a free tool to check cryptographic protocols that helps in searching and characterization of attacks. The main advantage of this application is that allows different verification techniques using a same protocol. We can say, it is a graphical interface for managing HLPSL (High-Level Protocol Specification Language) and CAS + (an implementation of the Protocol Central Authentication), which allows the translation between these languages ​​and also provides a friendly graphical user interface. SPAN helps to produce interactively sequences messages or MSC (Message Sequence Charts).

This tool is used for simulating cryptographic protocol, allows active or passive intruder simulation, the automatic attack's construction of the designed protocols. The protocol can be edited by means of HLPSL or CAS+, having the ability to convert between these languages. Some features of the graphical user interface are shown in Figure # 1.

Figure # 1: SPAN GUI description.