A domain-specific language for cryptographic protocols based on streams

Developing security-critical systems is difficult and there are many well-known examples of security weaknesses exploited in practice. Thus a sound methodology supporting secure systems development is urgently needed. In particular, an important missing link in the construction of secure systems is finding a practical way to create reliably secure crypto protocol implementations. We present an approach that aims to address this need by making use of a domain-specific language for crypto protocol implementations. One can use this language to construct a compact and precise yet executable representation of a cryptographic protocol. This high-level program can be verified against the security goals using automated theorem provers for first order logic. One can then use it to provide assurance for legacy implementations of crypto protocols by generating test-cases.