Secrecy by typing in the computational model

Stéphanie Delaune (1, 2, 3) , Clément Herouard (1, 2, 3) , Joseph Lallemand (1, 3, 2)

1 SPICY - Security & PrIvaCY
2 IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
3 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires

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 (\ie concatenation). Our approach has the usual benefit 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.

Mots clés: security protocols; formal methods; verification; computational models

Domaines: Cryptographie et sécurité [cs.CR]

Stéphanie Delaune, Clément Herouard, Joseph Lallemand. Secrecy by typing in the computational model. 38th IEEE Computer Security Foundations Symposium (CSF 2025), Owen Arden, Jun 2025, Santa Cruz, CA, United States. ⟨hal-04666965⟩