Abstract
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 \(\mathcal{P}\) that satisfies certain security properties can be assured to retain these properties after it is “wrapped” in a protocol \(\mathcal{W}[\mathcal{P}]\) 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the Pi Calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 340–354. Springer, Heidelberg (2004)
Agha, G., Frolund, S., Panwar, R., Sturman, D.: A Linguistic Framework for Dynamic Composition of Dependability Protocols. IEEE Parallel and Distributed Technology: Systems and Applications 1, 3–14 (1993)
Agha, G., Greenwald, M., Gunter, C.A., Khanna, S., Meseguer, J., Sen, K., Thati, P.: Formal modeling and analysis of dos using probabilistic rewrite theories. In: Foundations of Computer Security (FCS 2005) (2005)
Alpern, B., Schneider, F.B.: Defining Liveness. Information Processing Letters 21(4), 181–185 (1985)
Armando, A., et al.: The Avispa Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Backes, M., Pfitzmann, B., Waidner, M.: A Composable Cryptographic Library with Nested Operations. In: 10th ACM conference on Computer and Communications Security, pp. 220–230 (2003)
Bernstein, D.J.: SYN cookies (1996), http://cr.yp.to/syncookies.html
Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: 12-th IEEE Computer Security Foundations Workshop, pp. 55–69 (1999)
Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A Derivation System and Compositional Logic for Security Protocols. J. Comput. Secur. 13(3), 423–482 (2005)
Denker, G., Meseguer, J., Talcott, C.: Protocol Specification and Analysis in Maude. In: Workshop on Formal Methods and Security Protocols (1998)
Denker, G., Meseguer, J., Talcott, C.: Rewriting Semantics of Meta-Objects and Composable Distributed Services. In: 3rd. Intl. Workshop on Rewriting Logic and its Applications (2000)
Durgin, N., Mitchell, J.C., Pavlovic, D.: A Compositional Logic for Proving Security Properties of Protocols. J. Comput. Secur. 11(4), 677–721 (2004)
Escobar, S., Meadows, C., Meseguer, J.: A Rewriting-Based Inference System for the NRL Protocol Analyzer: Grammar Generation. In: Formal Methods in Security Engineering, pp. 1–12 (2005)
Fielding, R., Gettys, J., Mogul, J., Frystyk, H., Berners-Lee, T.: RFC 2068: Hypertext Transfer Protocol – HTTP/1.1. Internet Society, (1997)
Goguen, J.A., Meseguer, J.: Order-sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science 105(2), 217–273 (1992)
Gong, L., Syverson, P.: Fail-stop Protocols: An Approach to Designing Secure Protocols. In: 5th International Working Conference on Dependable Computing for Critical Applications, pp. 44–55 (1995)
Goodloe, A.E., Gunter, C.A.: Reasoning about Concurrency for Security Tunnels. In: IEEE Computer Security Foundations (CSF 2007) (2007)
Gunter, C.A., Khanna, S., Tan, K., Venkatesh, S.S.: DoS Protection for Reliably Authenticated Broadcast. In: Network and Distributed System Security Symposium (2004)
Gupta, A., Shmatikov, V.: Security Analysis of Voice-over-IP Protocols. Computer Security Foundations Symposium 00, 49–63 (2007)
Harkins, D., Carrel, D.: The Internet Key Exchange(IKE). Internet Society (1998)
He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A Modular Correctness Proof of IEEE 802.11i and TLS. In: 12th ACM conference on Computer and Communications Security, pp. 2–15 (2005)
Kaufman, C.: RFC 4306: Internet Key Exchange (IKEv2) Protocol. Internet Society (2005)
Khanna, S., Venkatesh, S.S., Fatemieh, O., Khan, F., Gunter, C.A.: Adaptive Selective Verification. In: IEEE Conference on Computer Communications (INFOCOM 2008) (2008)
Lafrance, S., Mullins, J.: An Information Flow Method to Detect Denial of Service Vulnerabilities. Journal of Unified Computer Science 9(11), 1350–1369 (2003)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: Conference on Logic of Programs, pp. 196–218 (1985)
Mahimkar, A., Shmatikov, V.: Game-based Analysis of Denial-of-Service Prevention Protocols. In: 18th IEEE workshop on Computer Security Foundations, pp. 287–301 (2005)
Maughan, D., Schertler, M.M., Schneider, Turner, J.: Internet Security Association and Key Management Protocol (ISAKMP). Internet Society (1998)
Meadows, C.: A Formal Framework and Evaluation Method for Network Denial of Service. In: 12th IEEE workshop on Computer Security Foundations (1999)
Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Meseguer, J., Talcott, C.: Semantic Models for Distributed Object Reflection. In: 16th European Conference on Object-Oriented Programming, pp. 1–36. Springer, Heidelberg (2002)
Mitchell, J., Durgin, N., Lincoln, P., Scedrov, A.: Multiset Rewriting and the Complexity of Bounded Security Protocols. Journal of Computer Security 12(2), 247–311 (2004)
Piper, D.: The Internet IP Security Domain Of Interpretation for ISAKMP. Internet Society (1998)
Schuba, C.L., Krsul, I.V., Kuhn, M.G., Spafford, E.H., Sundaram, A., Zamboni, D.: Analysis of a Denial of Service Attack on TCP. In: IEEE Symposium on Security and Privacy, pp. 208–223 (1997)
Sistla, A.P.: Safety, Liveness and Fairness in Temporal Logic. Formal Asp. Comput. 6(5), 495–512 (1994)
Yu, C.-F., Gligor, V.D.: A Specification and Verification Method for Preventing Denial of Service. IEEE Transactions on Software Engineering 16(6), 581–592 (1990)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chadha, R., Gunter, C.A., Meseguer, J., Shankesi, R., Viswanathan, M. (2008). Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers. In: Barthe, G., de Boer, F.S. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2008. Lecture Notes in Computer Science, vol 5051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68863-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-68863-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68862-4
Online ISBN: 978-3-540-68863-1
eBook Packages: Computer ScienceComputer Science (R0)