Modelling Agent-Skipping Attacks in Message Forwarding Protocols

TL;DR

This paper models agent-skipping attacks in message forwarding protocols, analyzing their security implications and identifying vulnerabilities in modern protocols using a symbolic multiset rewriting framework.

Contribution

It introduces a comprehensive symbolic framework for modeling path protocols and security goals related to message integrity in agent-based forwarding systems.

Findings

Identifies key vulnerabilities in modern message forwarding protocols.

Highlights attacks that violate path integrity.

Provides a formal analysis framework for agent-skipping attacks.

Abstract

Message forwarding protocols are protocols in which a chain of agents handles transmission of a message. Each agent forwards the received message to the next agent in the chain. For example, TLS middleboxes act as intermediary agents in TLS, adding functionality such as filtering or compressing data. In such protocols, an attacker may attempt to bypass one or more intermediary agents. Such an agent-skipping attack can the violate security requirements of the protocol. Using the multiset rewriting model in the symbolic setting, we construct a comprehensive framework of such path protocols. In particular, we introduce a set of security goals related to path integrity: the notion that a message faithfully travels through participants in the order intended by the initiating agent. We perform a security analysis of several such protocols, highlighting key attacks on modern protocols.