Proof of Logic: Correctness of Next Generation Security Mechanisms (INTERNATIONAL JOURNAL OF COMPUTERS & TECHNOLOGY, 2013)
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.