Compositional logic for proof of correctness of proposed UDT security mechanisms

Publication Type:
Conference Proceeding
Proceedings - International Conference on Advanced Information Networking and Applications, AINA, 2012, pp. 686 - 694
Issue Date:
Filename Description Size
Thumbnail2012004351OK.pdf344.39 kB
Adobe PDF
Full metadata record
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. © 2012 IEEE.
Please use this identifier to cite or link to this item: