Secrecy by typing in the computational model - INRIA - Institut National de Recherche en Informatique et en Automatique
Conference Papers Year : 2025

Secrecy by typing in the computational model

Abstract

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.
Fichier principal
Vignette du fichier
main-long.pdf (702.2 Ko) Télécharger le fichier
CaseStudies.tar.gz (11.79 Ko) Télécharger le fichier
Squirrel.tar.gz (1.35 Mo) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04666965 , version 1 (02-08-2024)

Identifiers

  • HAL Id : hal-04666965 , version 1

Cite

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⟩
461 View
41 Download

Share

More