Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers

Current research on verifying security properties of communication protocols has focused on proving integrity and confidentiality using models that include a strong Man-in-the-Middle (MitM) threat. By contrast, protection measures against Denial-of-Service (DoS) must assume a weaker model in which an adversary has only limited ability to interfere with network communications. This paper demonstrates a modular reasoning framework in which a protocol P that satisfies certain security properties can be assured to retain these properties after it is "Wrapped" in a protocol W[P] that adds DoS protection.