Compositional Logic for Proof of Correctness of Proposed UDT Security Mechanisms

Abstract

We present an approach to analyze the applicability and secrecy properties of the selected security mechanisms when implemented with UDT. This approach extends applicability refinement methodology with symbolic model in UDT implementations. In our approach, we carry out a formal proof of correctness, therefore, determining applicability, using formal composition logic. This approach is modular, comprising a separate proof of each protocol section and providing insight into the network environment in which each section can be reliably employed. Moreover, the proof holds for a variety of failure recovery strategies and other implementation and configuration options. We derive our technique from the protocol composite logic on TLS and Kerberos in the literature. We, maintain, however, the novelty of our work for UDT specifically our newly developed mechanisms such as UDT-AO, UDT-DTLS, UDT-Kerberos(GSS-API) specifically for UDT.