User-friendly Formal Methods for Security-aware Applications and Protocols

Formal support in the design and implementation of security-aware applications increases the assurance in the final artifact. Formal methods techniques work by setting a model that unambiguously defines attacker capabilities, protocol parties behavior, and expected security properties. Rigorous reasoning can be done on the model about the interaction of the external attacker with the protocol parties, assessing whether the security properties hold or not. Unfortunately, formal verification requires a high level of expertise to be used properly and, in complex systems, the model analysis requires an amount of resources (memory and time) that are not available with current technologies. The aim of this thesis is to propose new interfaces and methodologies that facilitate the usage of formal verification techniques applied to security-aware protocols and distributed applications. In particular, this thesis presents: (i) Spi2JavaGUI, a framework for the model-driven development of security protocols, that combines (for the first time in literature) an intuitive user interface, automated formal verification and code generation; (ii) a new methodology that enables the model-driven development and the automated formal analysis of distributed applications, which requires less resources and formal verification knowledge to complete the verification process, when compared to previous approaches; (iii) the formal verification of handover procedures defined by the Long Term Evolution (LTE) standard for mobile communication networks, including the results and all the translation rules from specification documents to formal models, that facilitates the application of formal verification to other parts of the standard in the future