Formally Verifying Undetectability in Hidden Communication Systems with Maude-HCS
|
ABSTRACT A hidden communication system (HCS) embeds hidden messages within ordinary network activity by repurposing existing protocols as subliminal channels. Although prior work provides useful tools for assessing the detectability of the HCS, there is no general and modular framework that both formalizes what it means for an HCS to be undetectable and formally verifies that a concrete implementation satisfies this property. |