TY - GEN
T1 - Modular preservation of safety properties by cookie-based DoS-protection wrappers
AU - Chadha, Rohit
AU - Gunter, Carl A.
AU - Meseguer, Jose
AU - Shankesi, Ravinder
AU - Viswanathan, Mahesh
PY - 2008
Y1 - 2008
N2 - 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. In this paper we demonstrate a modular reasoning framework in which a protocol that satisfies certain security properties can be assured to retain these properties after it is "wrapped" in a protocol that adds DoS protection. This modular wrapping is based on the "onion skin" model of actor reflection. In particular, we show how a common DoS protection mechanism based on cookies can be applied to a protocol while provably preserving safety properties (including confidentiality and integrity) that it was shown to have in a MitM threat model.
AB - 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. In this paper we demonstrate a modular reasoning framework in which a protocol that satisfies certain security properties can be assured to retain these properties after it is "wrapped" in a protocol that adds DoS protection. This modular wrapping is based on the "onion skin" model of actor reflection. In particular, we show how a common DoS protection mechanism based on cookies can be applied to a protocol while provably preserving safety properties (including confidentiality and integrity) that it was shown to have in a MitM threat model.
UR - http://www.scopus.com/inward/record.url?scp=46049086600&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=46049086600&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-68863-1_4
DO - 10.1007/978-3-540-68863-1_4
M3 - Conference contribution
AN - SCOPUS:46049086600
SN - 3540688625
SN - 9783540688624
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 39
EP - 58
BT - Formal Methods for Open Object-Based Distributed Systems - 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings
T2 - 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2008
Y2 - 4 June 2008 through 6 June 2008
ER -