A Tool of Analysis and Implementation of Security Protocols on Distributed Systems

摘要

In this paper we present an analysis and automatic implementation tool of security protocols based on Techniques of Formal Description. A sufficiently complete and concise formal specification that has allowed us to define the state machine that corresponds to a cryptographic protocol has been designed to achieve our goals. This forma! specification also makes it possible to incorporate in a flexible way the mechanisms and functions of security. Our system makes it possible to automatically translate formal specifications of protocols to a group of derivation Prolog rules. Our work improves the solution first proposed by J.K. Millen in [1]. We study the vulnerability of security protocols exploring, in an automatic way, all its possible behaviors in agreement both with their formal specification and with the information potentially recorded by an intruder. As a result of our work, for example, the vulnerability of security protocols that is already proven in a theoretical way (Needhman-Schroeder protocol or SSH or AKA protocols) can be proven and analyzed automatically starting from the translation to rules of those protocols. Additionally, our tool incorporates a new concept of implementation of protocols based on the interpretation of formal specifications on distributed systems.