Secure Implementation of Cryptographic Protocols: A Case Study of Mutual Distrust

Security protocols are critical for protecting modern communication infrastructures and are therefore subject to thorough analysis. However practical implementations of these protocols lack the same level of attention and thus may be more exposed to attacks.This paper discusses security assurance provided by security-typedlanguages when implementing cryptographic protocols. Our results arebased on a case study using Jif, a Java-based security-typed language,for implementing a non-trivial cryptographic protocol that allowsplaying online poker without a trusted third party.The case study deploys the largest program written in a security-typedlanguage to date and identifies insights ranging from securityguarantees to useful patterns of secure programming