Protocol Dialects as Formal Patterns: A Composable Theory of Lingos -- Technical report
Víctor García, Santiago Escobar, Catherine Meadows, Jose Meseguer
TL;DR
This work develops a formal theory of lingos—parametric message transformations—and a modular dialect framework that uses lingos to fortify protocols against on-path attackers. It introduces f-checkable, authenticating, and malleable lingos, and defines four lingo-composition operators (horizontal, functional, data-adaptor, Cartesian products/tupling) to automatically synthesize stronger lingos and dialects. The authors provide executable Maude specifications and demonstrate concepts on MQTT, highlighting a path toward lightweight, composable, and verifiable first-line security layers. The framework supports dialects that wrap existing protocols without invasive changes and points toward non-malleable designs and formal security analysis via probabilistic model checking. Overall, the approach offers a rigorous, reusable foundation for creating moving-target security through protocol dialects and lingos with practical realizations.
Abstract
Protocol dialects are methods for modifying protocols that provide light-weight security, especially against easy attacks that can lead to more serious ones. A lingo is a dialect's key security component by making attackers unable to "speak" the lingo. A lingo's "talk" changes all the time, becoming a moving target for attackers. We present several kinds of lingo transformations and compositions to generate stronger lingos from simpler ones, thus making dialects more secure.