Redesigning secure protocols to compel grammatical compliance checking

Abstract

A frequent goal of LangSec research is to demonstrate the benefits of having protocol definitions whose messages can have their grammar checked to ensure that they are well-formed prior to any other processing. It is generally taken as a given that although we can design protocols which enable this checking, we cannot compel implementers of these protocols to actually carry out these checks. In this paper we demonstrate that it is possible to modify the protocols through the use of encryption such that the implementer is essentially required to do the checking if they wish their implementation to interoperate with other implementations without errors. Crucially, this will be the case even when they are only sending and receiving well-formed messages, thus transforming the silent vulnerability of unchecked messages into an obvious error. In specific, we demonstrate how to do this for checking whether or not messages or portions thereof belong to a specified regular language and whether or not they belong to a specified context-free language.