Compositional Logic for Proof of Correctness of Proposed UDT Security Mechanisms

Publisher:
IEEE
Publication Type:
Conference Proceeding
Citation:
2012 IEEE 26th International Conference on Advanced Information Networking and Applications (AINA), 2012, pp. 686 - 694
Issue Date:
2012-01
Full metadata record
Files in This Item:
Filename Description Size
Thumbnail2012004351OK.pdf344.39 kB
Adobe PDF
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.
Please use this identifier to cite or link to this item: