Proof of Logic: Correctness of Next Generation Security Mechanisms

Danilo Valeros Bernardo

doi:10.24297/ijct.v9i1.4156

Authors

Danilo Valeros Bernardo Db2Powerhouse, University of Technology - Sydney

DOI:

https://doi.org/10.24297/ijct.v9i1.4156

Keywords:

UDT, UDT-AO, UDT-DTLS, GSS-API, High-speed networks, PCL

Abstract

In this paper, three security mechanisms developed to form the UDT (UDP-Data Transfer protocol) Security Architecture are evaluated and analyzed. An approach is utilized to ascertain the applicability and secrecy properties of the selected security mechanisms when implemented with UDT. In this approach, a formal proof of correctness, through formal composition logic is carried out. This approach is modular; it has a separate proof for each protocol section that provides 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.

This paper is anÂ extension and a revised version of the works published by the author.

Downloads

Download data is not yet available.

Author Biography

Danilo Valeros Bernardo, Db2Powerhouse, University of Technology - Sydney

Dr. Danilo Valeros Bernardo is an honorary researcher of a non-for profit organisation in Australasia. He holds a degree in Computer Engineering (UC), Masters degree in Technology and Business (UNSW), Applied Sciences (Harvard) and PhD in Computer Science (UTS).