Secrecy by Typing in the Computational Model

In this paper, we propose a way to automate proofs of cryptographic protocols in the computational setting. We focus on non-deducibility – a weak notion of secrecy – and we aim to use type systems. Techniques based on typing were mainly used in symbolic models, and we show how they can be adapted to the Ccsa framework to obtain computational guarantees. We consider for now a fixed set of primitives, namely symmetric and asymmetric encryption, as well as pairing (i.e. concate-nation). Our approach has the usual benefits of type systems: it is modular, allows the security analysis for an unbounded number of sessions, and could be extended to other primitives (e.g. hashing) without excessive difficulties. We successfully applied our framework on several protocols from the literature and the ISO/IEC 11770 standard.