Redesigning secure protocols to compel security checks

Abstract

In the study of secure protocols, we must both ensure that the design of the protocol is secure and that the implementation is correct. One implementation problem which has frequently occurred is that implementations fail to implement some of the checks which are needed for the protocol to be secure. For example, implementations may fail to validate certificates or fail to validate all aspects of the certificate. In this paper, we demonstrate that it is possible to change the design of a protocol to compel the implementation to carry out the checks. We assume that programmers will always do at least what is necessary to read and produce properly formatted messages. Then we use some simple cryptography to ensure that reading properly formatted messages essentially requires checking the parameters.