Cryptographic Web Applications: from Security Engineering to Formal Analysis

We overview the most significant security issues in cryptographic web applications and review the solutions proposed in the literature. We focus in particular on principled techniques amenable to formal verification, for two reasons. First, cryptographic web applications are expected to satisfy strong security and privacy requirements, hence provably sound (or at the very least rigorous) guarantees are desirable. Second, the complexity of the web platform and the huge extension of the attack surface against cryptographic web applications call for a systematic, formal assessment of the entire implementation stack from specification to production code.