02.06.2025
Polycrypt: Beyond the Linicrypt model
Abstract
The Linicrypt framework (Carmer and Rosulek, Crypto’16) provides a foundation for systematic, automated reasoning about cryptographic programs whose primitive instructions include randomly sampling, evaluating linear combinations, and querying a random oracle over some known finite field. Later, McQuoid et al. (TCC’19) gave a characterization of collision and second-preimage resistance for a class of programs, for which such properties can be checked in polynomial time. Other works have then extended similar characterizations to alternative notions either in the pseudo-random permutation (PRP) or in the ideal cipher (IC) model. None of these variations provides a way to reason about programs which employ non-linear operations over their state.
In this talk we will introduce the Polycrypt framework, an extension of Linicrypt which admits the evaluation of arbitrary polynomial transformations over the underlying field. We show how to algebraically represent such programs, and in particular we demonstrate how it naturally allows us to model important security properties such as collision and second preimage resistance. We characterize a class of “sparse” programs which admits a polynomial-time algorithm to establish collision/second-preimage resistance. We also show that Polycrypt can be readily extended to the IC model, where it can be employed to automatically verify security properties of constructions that intrinsically make use of non-linear components, such as the Galois Counter Mode (GCM) and extensions thereof.
The Linicrypt framework (Carmer and Rosulek, Crypto’16) provides a foundation for systematic, automated reasoning about cryptographic programs whose primitive instructions include randomly sampling, evaluating linear combinations, and querying a random oracle over some known finite field. Later, McQuoid et al. (TCC’19) gave a characterization of collision and second-preimage resistance for a class of programs, for which such properties can be checked in polynomial time. Other works have then extended similar characterizations to alternative notions either in the pseudo-random permutation (PRP) or in the ideal cipher (IC) model. None of these variations provides a way to reason about programs which employ non-linear operations over their state.
In this talk we will introduce the Polycrypt framework, an extension of Linicrypt which admits the evaluation of arbitrary polynomial transformations over the underlying field. We show how to algebraically represent such programs, and in particular we demonstrate how it naturally allows us to model important security properties such as collision and second preimage resistance. We characterize a class of “sparse” programs which admits a polynomial-time algorithm to establish collision/second-preimage resistance. We also show that Polycrypt can be readily extended to the IC model, where it can be employed to automatically verify security properties of constructions that intrinsically make use of non-linear components, such as the Galois Counter Mode (GCM) and extensions thereof.