In the last few years there have been rapid developments in SMT solving for finite fields. These include new decision procedures, new implementations of SMT theory solvers, and new software verifiers that rely on SMT solving for finite fields. To support interoperability in this emerging ecosystem, we propose the SMT-LIB theory of finite field arithmetic (FFA). The theory defines a canonical representation of finite field elements as well as definitions of operations and predicates on finite field elements.
Finite fields are the basis for a large body of security-critical code. They are used in public-key
cryptography: elliptic curves over finite fields are used in nearly all web browser connections for key exchange
or digital signatures [
The importance and prevalence of (finite-)field-based programs creates a need for tools that can
formally verify them. Ideally, such tools would be partially or fully automated. The natural approach
is SMT-based verification , as taken by prior tools like Dafny [
One way to solve field equations is by encoding them as integer equations, which many SMT solvers
already comprehend. Consider (for the moment) a finite field of prime order . Such a field is isomorphic
to the integers {0, . . . , − 1} with addition and multiplication modulo [
To overcome the limitations of encoding, two direct SMT theory solvers for finite fields have recently
emerged. The first is an MCSat [ 19] solver that is implemented in Yices [20, 21, 22, 23, 24]. The second is
a CDCL(T) solver that is implemented in cvc5 [
These SMT solvers have already enabled a variety of research projects and tools for automatically verifying systems that use zero-knowledge proofs (ZKPs). One project builds an automatically verifiable compiler pass for CirC: a compiler used with ZKPs [27]. Another builds a tool QED2 that automatically verifies ZKP code in the Circom language [ 28, 29]. Another builds a tool for automatically verifying
ZKP code written using the Halo2 library [30]. All of these projects use an SMT solver with finite field support.
Given the long-term importance of finite fields to security-critical software, the emergence of multiple SMT solvers with finite field support, and the emergence of multiple automatic verification tools expecting finite field support, we think the time is ripe to specify finite fields as an SMT-LIB theory. In this short paper, we do exactly that. In our specification, we consider all finite fields: those of prime order and their extensions. We consider fields of arbitrary size. Many cryptosystems require large fields (such as a prime order field with ≈ 2256 or the binary extension field of order 2128), but some can also operate over smaller fields (such as 32-bit or 64-bit fields) [31, 32].
Related Work There is already much work on verifying cryptographic implementations through interactive theorem proving and verification languages. Examples of secret-key and public-key cryptography include Fiat cryptography [33], Easycrypt [34], HACL* [35], and Jasmin [36]. There is also some work on interactive verification for ZKPs in the context of the Leo compiler [ 37], and by using refinement proofs [ 38, 39]. With better SMT-level support for finite fields, ITP proof automation for ifnite field lemmas could be improved through ITP-SMT bridges, like SMTCoq [40].
Further afield, some cryptographic implementations have been modeled and analyzed using automated symbolic analysis tools like Tamarin [41] and ProVerif [42]. The benefit of these tools is their high level of interpretability and automation, which allows them to be applied to protocols of realistic complexity, such as Signal [43]. However, they struggle to accurately model algebraic structures [44]. SMT-level algebraic reasoning would complement this research.
Another line of research develops SMT solvers for non-linear integer and real arithmetic using CDCL(T) [45, 46, 47, 48, 49, 50, 51, 52] and MCSat [53, 54, 55]. Some works specifically consider local search [56, 57, 58] and quantifier elimination [ 59, 60]. This research serves as good inspiration into techniques for finite field solving.
We provide a brief summary of the relevant concepts of finite fields. A comprehensive overview can be found in [61, 62, 63] as well as in many other algebra textbooks.
Fields. A field F consists of a set of elements on which the two binary operators addition “+” and multiplication “· ” are defined. is closed under both operators, i.e. when applied on two elements of , the result is in . Both operators are commutative, associative, and have distinct neutral elements (denoted as zero (0) and one (1), respectively). Each element in has an additive inverse element and all elements in ∖ {0} have a multiplicative inverse element. Further, distributivity of multiplication over addition holds. Informally speaking, a field is a set with well-defined operations addition, subtraction, multiplication, and division (with the exception of division by 0). Well known examples of fields are the rational number Q and the real numbers R.
Finite Fields. A field F where is finite is called a finite field .1 The size of is the order of F. It has been shown that every finite field has order that is a prime power = . We distinguish between prime fields with = 1 and extension fields with > 1. All fields of equal order are isomorphic (i.e. equivalent up to relabelling of elements), thus the field of order is unique (up to isomorphism). Prime Fields. The prime field of order can be represented as = {− ⌊︁ − 2 1 ⌋︁, . . . , 0, 1, . . . , ⌊︀ 2 ⌋︀ }2 and is denoted F. Let the function smod : Z → be defined to map ∈ Z to the unique element 1In honor of French mathematician Évariste Galois, finite fields are also called Galois fields . 2In the (isomorphic) representation = {0, . . . , − 1}, (with addition and multiplication modulo ), small “negative” values (such as − 1) are instead represented as large positive values (such as − 1), which can be unintuitive to read. We choose our representation because small negative values are common in many applications. of that is equivalent to , modulo . The function is called “smod” because it outputs a signed representation of its input.
Addition and multiplication on are defined by the usual integer operations followed by an application of smod. Due to the construction of , finding the additive inverse is as simple as flipping the sign (assuming odd ).
Example 1. The finite field F5 can be represented by the integers {− 2, − 1, 0, 1, 2}. In this representation of F5, 2 + 1 = − 2, 2 · (− 1) = − 2, and (2 + 1) · 2 = 1 hold.
Extension Fields. Let F[ ] be the set of univariate polynomials in variable with coeficients from F, and let ∈ F[ ] have degree and be irreducible (i.e. it cannot be represented as the product of two non-constant polynomials). The extension field of order is denoted F and can be represented as polynomials in F[ ] of degree less than , with (polynomial) addition and multiplication modulo . Note that, in this representation, {0, 1} ⊆ F ⊆ F .
Example 2. The finite field
F32 is represented by the following polynomials of F3[ ] modulo 2 − − 1: {0, ,
+ 1, − + 1, − 1, − , − − 1, − 1, 1} Over F32 it holds that ( + 1) · = (− + 1).
As the choice of is not unique in general, diferent (isomorphic) representations of F exist, even if the representation of F is fixed. Note that no finite field is an ordered field . That is, there is no total ordering on that is compatible with the field operations.
Conway Polynomials Algebraic tools have many choices for how to represent fields internally. But, to facilitate interoperability, the computer algebra community has agreed upon a canonical family of irreducible polynomials that should be used to represent elements of an extension field F in tool interfaces. These are called the Conway polynomials , ∈ F[ ], where is a prime and > 1. The precise definition of the Conway polynomials is not important for our purposes. 3 There is an algorithm for finding them [ 64] and they have been pre-computed for many and [65]. The Conway polynomials are used by all prominent computer algebra libraries: Sage, Magma, GAP, Singular, etc. We will use the Conway polynomials to define an SMT-LIB syntax for extension field element literals (Sec. 3.3).
Example 3. The Conway polynomial 3,2 is 2 − − 1, which is the irreducible used to represent F9 in Example 2.
This section presents the SMT-LIB (version 2.6) theory of finite field arithmetic theory of finite field arithmetic are the logics of quantifier-free finite field arithmetic its quantified version FFA. (FFA). Based on the
QF_FFA as well as 3The Conway polynomial , is the lexicographically minimal monic primitive polynomial of degree over F that is compatible with , for all dividing . Let = ( − 1)/( − 1) (which is an integer). Then, , ∈ F[ ] is compatible with , ∈ F[ ] if for every root 0 ∈ F of the former, 0 is a root of the latter. The lexicographic ordering used is also slightly non-standard. Define the alternating-sign coeficient representation of polynomial ∈ F[ ] to be = ∑︀=0(− 1)− − = − − 1 − 1 + · · · + (− 1)0, with ∈ {0, . . . , − 1}. Then, the order is lexicographic over the tuples (, . . . , 0).
The theory of finite fields defines two kinds of finite field sorts, prime field sorts and extension field sorts for prime and extension fields, respectively (Sec. 2). They are represented by an indexed sort identifier of the form (_ FiniteField ) and (_ FiniteField ) for prime and extension field sorts, respectively. The indexes and are numerals specifying the finite field order = . The index must be a prime number in both cases. For extension field sorts, > 1 must hold, as otherwise the resulting sort would be a prime field. Providing a non-prime number as may result in unspecified solver behavior, although solvers are encouraged to report an error.4 As is usual for an indexed sort, two finite field sorts with a diferent order are diferent sorts. Solvers implementing this theory are not required to support extension field sorts and may report an error in case an extension field sort is specified. 5
For the rest of this chapter, a finite field sort is a prime or extension efild sort with an arbitrary fixed order.
Example 4. Set the logic to non-linear finite field arithmetic and define finite field sorts of size 5 and 9: (set-logic QF_FFA) (define-sort FF5 () (_ FiniteField 5)) (define-sort FF9 () (_ FiniteField 3 2))
A finite field of a given order is uniquely defined up to isomorphism. Thus, for the sake of defining an SMT theory for finite fields, a canonical representation for a finite field of a given order needs to be ifxed. Otherwise diferent solvers might present the same model diferently.
For a prime field with prime order , the elements are represented by the integers of the set {− ⌊︁ − 2 1 ⌋︁, . . . , ⌊︀ 2 ⌋︀ }. Operations are performed with regard to the function smod as defined in Section 2. For an extension field of order the field elements are represented by univariate polynomials over the prime field of order . The implied field is F[ ]/,, where , is the Conway polynomial (Sec. 2). All polynomial operations are performed modulo the Conway polynomial ,.
In the theory of finite fields, each element of a finite field sort is represented by a literal. To avoid confusion with the theories of integer and reals, finite field literals are prefixed with the string ff. We further say that a literal is normalized when it stands for an element from the fixed field representation as defined in Section 3.2. Non-normalized literals are allowed as an input and are mapped to the corresponding normalized literal, however, solvers are required to resort to normalized literals when printing a value.
Prime field literals. As stated in Section 2, elements of prime fields can be represented as integers modulo the field size. This property is used to define literals in the form of ff , where is an integer value. Given a prime field sort (_ FiniteField ) with prime order , elements represented by the literals ff for all values ∈ {− ⌊︁ − 2 1 ⌋︁, . . . , ⌊︀ 2 ⌋︀ } are normalized. Every literal outside this set is mapped to the corresponding normalized literal by utilizing smod( ). Using this operation, the input gets mapped to the (unique) normalized representative of the same congruence class modulo . In the 4We recommend that solvers test ’s primality probabilistically, for example with a 40-repetition Miller-Rabin test [66]. If is not prime, the solver can report an error. If is prime or if the test is inconclusive, the solver may assume that is prime and continue. 5We choose diferent syntaxes for prime fields and their extensions so that a user who is only interested in prime fields need not understand or even be aware of extension fields.
field type prime field extension field order syntax (_ ff ) ff m (as ff (_ FiniteField )) syntax type indexed shorthand annotated (_ ff .· · · . ) indexed ff .· · · . mp shorthand (as ff .· · · . (_ FiniteField )) annotated presence of finite field theory, the user may not define their own symbols of form shadow other theory-defined symbols). ff (nor may they Example 5. Given the defined sorts of Example 4, then examples of normalized elements of FF5 are ff1, ff0, and ff-2. The (non-normalized) literals ff4 and ff10 describe the same element as the normalized literals ff-1 and ff0, respectively.
Extension field literals. Elements of extension field sorts are polynomials. Literals representing elements of extension field sorts are uniquely describing polynomials by specifying their coeficients. As described in Section 2, an element of a finite field of order = with > 1 is a polynomial ∈ F[ ] of degree at most − 1. Let = 0 + 1 1 + · · · + − 1 − 1 where ∈ F, then the element is represented by the literal ff0.1.· · · .− 1 where all are integers. Tailing zeros may be omitted, e.g. in (_ FiniteField 3 6) the literals ff1.0.-1.0.0 and ff1.0.-1 both represent the element 1 − 2. This further ensures that elements in F ⊆ F have the same literal representation in both (_ FiniteField ) and (_ FiniteField ). A (polynomial) literal of (_ FiniteField ) is normalized when all integer coeficients are normalized with regard to and all tailing zeros are omitted. Specifying a literal with more than coeficients is invalid. Example 6. Again, given the defined sorts of Example 4, normalized literals of FF9 are all (normalized) literals of (_ FiniteField 3): ff0, ff1, and ff-1, as well as literals representing the further (polynomial) elements of F32 , for example ff-1.1, ff0.1, and ff-1.-1 representing the elements − 1, , and − − 1, respectively. Note that ff2.1 and ff1.0 are both non-normalized versions of ff-1.1 and ff1, respectively.
Well-Sortedness of literals. Since the defined literals are overloaded (for example, every finite field has a one element, thus ff1 is of undetermined sort), the order of the literal’s field must be specified in order to satisfy the well-sortedness requirements of SMT-LIB. There are three ways of specifying the sort of a finite field literal. (i) By indexing the literal (_ ff. . . ) and (_ ff. . . ) with the finite ifeld order and , respectively. This allows the literal’s sort to be derived, as the order of the finite ifeld specifies the sort uniquely. (ii) Similar to the theory of bit-vectors, there is a shorthand to avoid the _ keyword and specify the sort as part of the literal symbol. This is done by appending the literal with m and mp for prime field sort of order and extension field sort of order , respectively.6 (iii) Since might be a large number, a short-cut is provided by (as ff. . . ) where is a finite field sort. Using the define-sort command, one can assign a symbol to a finite field sort to be used for all its literals. Table 1 gives an overview of all three variants. When printing finite field elements, solvers are free to choose between the first two notations.
Example 7. The expressions (_ ff1 5) and (_ ff1 3 2) denote the multiplicative identity (one) of F5 and F32 , respectively. In the shorthand notation, the same literals can be written as ff1m5 and ff1m3p2. Using the defined sorts from Example 4, (as ff1 FF5) and (as ff1 FF9) can be used alternatively. 6Here, “m” denotes modulo and “p” denotes power. But, note that F and Z are not isomorphic for > 1.
All of the following operator definitions represent well known semantics from algebra. Thus, an explicit definition of their semantics is omitted and we refer to Section 2 for further details. Operations always operate on one specific finite field sort , i.e. all parameters have sort and an element of is returned. All functions are defined for all prime field sorts as well as all extension field sorts. For the sake of brevity, the extension field sort variants of the functions are omitted. Table 2 gives an overview of all operations.
Binary arithmetic. For each finite field order, we define operations that take two finite field elements of one finite field sort and return an element of the same sort. Given two inputs, the operations represent sum, diference, product, and quotient, respectively. 7 (ff.add (_ FiniteField ) (_ FiniteField ) (_ FiniteField ) :left-assoc) (ff.sub (_ FiniteField ) (_ FiniteField ) (_ FiniteField )) (ff.mul (_ FiniteField ) (_ FiniteField ) (_ FiniteField ) :left-assoc) (ff.div (_ FiniteField ) (_ FiniteField ) (_ FiniteField )) As hinted by the :left-assoc keyword, occurrences of ff.add and ff.mul may contain more than two arguments and multiple arguments are grouped left associatively. However, note that both operations are associative anyway.8 Unary arithmetic. For each finite field sort, there are the following unary operations: (ff.neg (_ FiniteField ) (_ FiniteField )) (ff.recip (_ FiniteField ) (_ FiniteField ))
Here, ff.neg returns the unary negation (usually written as − for an element ), i.e. the inverse element with regard to addition. The operation ff.recip returns the reciprocal value (usually written as − 1 for an element ), i.e. the inverse element with regard to multiplication. Note that ff.recip has total semantics but is unspecified for the zero element.
Division by zero. Two operators (ff.div, ff.recip) represent mathematical operations with only partial semantics. Mathematically speaking, division by zero is undefined, and computing the reciprocal of zero is undefined. Yet, SMT-LIB requires functions to have total semantics. We require solvers to interpret the reciprocal of zero as zero. Moreover dividing any value by zero gives zero. This choice is somewhat arbitrary. It is acceptable because it easy for solvers to meet and for verification tools to use.
A solver can meet this requirement using a preprocessing transformation. First, it encodes division as multiplication by the divisor’s reciprocal. Second, it encodes the reciprocal relation = (ff.recip ) by the following (reciprocal-free) formula:
[( ̸= 0) ∧ ( = 1)] ∨ [( = 0) ∧ ( = 0)] This ensures that 0’s reciprocal is 0. The are other encodings of reciprocal that do not explicitly contain a disjunction. For example, as ( = ) ∧ ( = ).
This requirement is also easy for verification tools that use SMT to work with. In particular, a verification tool can create an SMT query where division or reciprocal have diferent semantics by wrapping them with an if-then-else term that implements those semantics when the appropriate input is zero. 7Since ff.neg and ff.recip are defined as well, ff.sub and ff.div are redundant. However, we believe that all common mathematical operations should have operations in the finite field theory. Furthermore, other arithmetic theories in SMT-LIB also define redundant subtraction and division operators. 8Note that ff.div is not Euclidean division, rather it is multiplication by an inverse in the field. Thus, the remainder of a division, i.e. ff.rem, would not be meaningful.
Meaning ff.add × → finite field addition ff.sub × → finite field subtraction ff.mul × → finite field multiplication ff.div × → finite field division ff.neg → finite field negation ff.recip → finite field reciprocal
Since finite fields are not ordered, the theory of finite fields only supports the equality predicate: (= (_ FiniteField ) (_ FiniteField )) (= (_ FiniteField ) (_ FiniteField )) Example 8. Continuing with the definition of Example 4. First define some variables: (declare-fun x0 () FF5) (declare-fun x1 () FF5) (declare-fun x2 () FF5) Then add some assertions: (assert (= (ff.mul x1 x2) (ff.add x1 x2))) (assert (= (ff.recip x1) x0)) (assert (= (ff.sub x2 x0)) (as ff1 FF5)) This encodes the constraint system in F5: 12 = 1 + 2 −1 1 = 0 2 − 0 = 1
There are two existing SMT solvers that support the theory of finite fields: Yices [ 23] and cvc5 [26]. Both support the logic of quantifier-free finite field arithmetic QF_FFA for prime fields as defined in this paper.
• Yices2 implements reasoning over prime fields using its MCSat engine [ 24]. This implementation
is based on the approach by Hader et al. [22]. Processing of polynomials over prime fields is done
done using an updated version of the LibPoly library [67].
• cvc5’s prime field solver is a CDCL( ) theory solver that implements two decision procedures
designed by Ozdemir et al. The first procedure is based on Gröbner bases and triangular
decomposition [
In designing our theory, we have intentionally omitted a number of potential features. Some of these features might be good additions in the future. We discuss two such features here, together with why they might be useful.
Conversions In this proposal, we do not give operations for converting between finite field elements and other discrete arithmetic types, such as integers and bit-vectors. This might be useful for veriifcation problems about code that converts between these types. For example, the AES-GCM block cipher alternates between treating its data as bit-vectors and elements of F2 , to perform diferent kinds of operations on that data. The bit-vector representation is used for the AES permutation and the field representation is used in the GCM message authentication code. Another example is an implementation of F arithmetic on a -bit CPU, where 2 ≪ . Such an implementation is defined by bit-vector arithmetic, but the specification is an equation in F. Thus, giving a natural statement of the implementation’s correctness requires operations to convert between F and bit-vectors. Since some SMT solvers already allow conversions between bit-vectors and integers, conversions between integers and finite field elements might sufice.
Another kind of conversion which might be useful is one between a field F and some extension F() of it (for > 1).
Variable-sized fields In this proposal, we consider only fields of fixed size. This bars the possibility of queries that verify a property that holds generically for many or all fields. Such properties arise naturally in many verification problems. For instance, one might have a function that implements some ifnite-field operation in which the size of the field is an input to the function. To verify the function for all fields, one might construct a logical formula in which the field size is a variable.
Acknowledgements. We thank Ahmed Irfan, Alp Bassa, Clark Barrett, Daniela Kaufmann, Gereon Kremer, Shankara Pailoor, Sorawee Porncharoenwase, and the SMT’24 reviewers for valuable discussion and feedback. We further thank Stéphane Graham-Lengrand for hosting the first author for a research stay at SRI during which the idea for this work initiated. We acknowledge funding from the TU Wien SecInt Doctoral College, NSF grant number 2110397, the Stanford Center for Automated Reasoning, and the Simons Foundation. [18] A. Niemetz, M. Preiner, Y. Zohar, Scalable bit-blasting with abstractions, in: CAV, 2024. [19] D. Jovanovic, C. Barrett, L. De Moura, The design and implementation of the model constructing satisfiability calculus, in: FMCAD, 2013. [20] T. Hader, Non-linear SMT-reasoning over finite fields, 2022. MSc Thesis (TU Wien). [21] T. Hader, L. Kovács, Non-linear SMT-reasoning over finite fields, in: SMT, 2022. URL:
http://ceur-ws.org/Vol-3185/extended3245.pdf , extended Abstract. [22] T. Hader, D. Kaufmann, L. Kovács, SMT solving over finite field arithmetic, in: LPAR, 2023. [23] B. Dutertre, Yices 2.2, in: CAV, 2014. [24] T. Hader, D. Kaufmann, A. Irfan, S. Graham-Lengrand, L. Kovács, MCSat-based Finite Field Reasoning in the Yices2 SMT
Solver, 2024. arXiv:2402.17927. [25] A. Ozdemir, S. Pailoor, A. Bassa, K. Ferles, C. Barrett, I. Dillig, Split Gröbner bases for satisfiability modulo finite fields, 2024. https://ia.cr/2024/572. [26] H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, Y. Zohar, cvc5: A versatile and industrial-strength SMT solver, in: TACAS, 2022. [27] A. Ozdemir, R. S. Wahby, F. Brown, C. Barrett, Bounded verification for finite-field-blasting, in: CAV, 2023. [28] S. Pailoor, Y. Chen, F. Wang, C. Rodríguez, J. Van Gefen, J. Morton, M. Chu, B. Gu, Y. Feng, I. Dillig, Automated detection of under-constrained circuits in zero-knowledge proofs, in: PLDI, 2023. [29] M. Bellés-Muñoz, M. Isabel, J. L. Muñoz-Tapia, A. Rubio, J. Baylina, Circom: A circuit description language for building zero-knowledge applications, IEEE Transactions on Dependable and Secure Computing (2022). [30] F. H. Soureshjani, M. Hall-Andersen, M. Jahanara, J. Kam, J. Gorzny, M. Ahmadvand, Automated analysis of Halo2 circuits, 2023. https://ia.cr/2023/1051. [31] P. Zero, Plonky2: Fast recursive arguments with Plonk and FRI, 2022.
https://github.com/0xPolygonZero/plonky2/blob/main/plonky2/plonky2.pdf . [32] E. Ben-Sasson, I. Bentov, Y. Horesh, M. Riabzev, Fast reed-solomon interactive oracle proofs of proximity, in: ICALP, 2018. [33] A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala, Simple high-level code for cryptographic arithmetic – with proofs, without compromises (2020). [34] G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt, P.-Y. Strub, Easycrypt: A tutorial, International School on
Foundations of Security Analysis and Design (2012) 146–166. [35] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, B. Beurdouche, HACL*: A verified modern cryptographic library, in:
CCS, 2017. [36] J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire, V. Laporte, T. Oliveira, H. Pacheco, B. Schmidt, P.-Y. Strub,
Jasmin: High-assurance and high-speed cryptography, in: CCS, 2017. [37] A. Coglio, E. McCarthy, E. W. Smith, Formal verification of zero-knowledge circuits, 2023. URL: http://dx.doi.org/10.4204/EPTCS.393.9. [38] J. Liu, I. Kretz, H. Liu, B. Tan, J. Wang, Y. Sun, L. Pearson, A. Miltner, I. Dillig, Y. Feng, Certifying zero-knowledge circuits with refinement types, arXiv preprint arXiv:2304.07648 (2023). [39] K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, T. Wies, Less is more: refinement proofs for probabilistic proofs, in:
IEEE S&P, 2023. [40] B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds, C. Barrett, SMTCoq: A plug-in for integrating SMT solvers into Coq, in: CAV, 2017. [41] S. Meier, B. Schmidt, C. Cremers, D. Basin, The TAMARIN prover for the symbolic analysis of security protocols, in: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings 25, Springer, 2013, pp. 696–701. [42] B. Blanchet, B. Smyth, V. Cheval, M. Sylvestre, ProVerif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018). [43] K. Cohn-Gordon, C. Cremers, B. Dowling, L. Garratt, D. Stebila, A formal security analysis of the Signal messaging protocol, Journal of Cryptology 33 (2020) 1914–1983. [44] C. Cremers, D. Jackson, Prime, order please! revisiting small subgroup and invalid curve attacks on protocols using
Difie-Hellman, in: CSF, 2019. [45] E. Ábrahám, J. H. Davenport, M. England, G. Kremer, Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119 (2021). [46] A. Cimatti, A. Griggio, A. Irfan, M. Roveri, R. Sebastiani, Experimenting on solving nonlinear integer arithmetic with incremental linearization, in: International Conference on Theory and Applications of Satisfiability Testing, Springer, 2018, pp. 383–398. [47] A. Maréchal, A. Fouilhé, T. King, D. Monniaux, M. Périn, Polyhedral approximation of multivariate polynomials using
Handelman’s theorem, in: VMCAI, 2016. [48] M. Fränzle, C. Herde, T. Teige, S. Ratschan, T. Schubert, Eficient solving of large non-linear arithmetic constraint systems with complex boolean structure, Journal on Satisfiability, Boolean Modeling and Computation 1 (2006). [49] V. X. Tung, T. V. Khanh, M. Ogawa, raSAT: An SMT solver for polynomial constraints, in: IJCAR, 2016. [50] D. Jovanović, L. d. Moura, Cutting to the chase solving linear integer arithmetic, in: CADE, 2011. [51] I. Dillig, T. Dillig, A. Aiken, Cuts from proofs: A complete and practical technique for solving linear inequalities over integers, 2009, pp. 233–247. [52] F. Corzilius, G. Kremer, S. Junges, S. Schupp, E. Ábrahám, SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving, in: SAT, 2015. [53] D. Jovanović, L. De Moura, Solving non-linear arithmetic, ACM Communications in Computer Algebra 46 (2013). [54] D. Jovanović, Solving nonlinear integer arithmetic with MCSAT, in: VMCAI, 2017. [55] L. d. Moura, D. Jovanović, A model-constructing satisfiability calculus, in: VMCAI, 2013. [56] S. Cai, B. Li, X. Zhang, Local search for satisfiability modulo integer arithmetic theories, ACM Transactions on
Computational Logic (2023). [57] X. Zhang, B. Li, S. Cai, Deep combination of CDCL (T) and local search for satisfiability modulo non-linear integer arithmetic theory, 2024. [58] Z. Wang, B. Zhan, B. Li, S. Cai, Eficient local search for nonlinear real arithmetic, in: VMCAI, 2023. [59] B. F. Caviness, J. R. Johnson, Quantifier elimination and cylindrical algebraic decomposition, Springer Science &
Business Media, 1998. [60] V. Weispfenning, Quantifier elimination for real algebra—the quadratic case and beyond, Applicable Algebra in
Engineering, Communication and Computing 8 (1997). [61] R. Lidl, H. Niederreiter, Introduction to finite fields and their applications, Cambridge university press, 1994. [62] R. J. McEliece, Finite fields for computer scientists and engineers, volume 23, Springer Science & Business Media, 2012. [63] J. A. Gallian, Contemporary Abstract Algebra, Chapman and Hall/CRC, 2021. [64] L. S. Heath, N. A. Loehr, New algorithms for generating conway polynomials over finite fields, Journal of Symbolic
Computation 38 (2004) 1003–1024. [65] F. Lübeck, Conway polynomials for finite fields, ???? Pre-computed Conway polynomials. Available at https://www.math.rwth-aachen.de/~Frank.Luebeck/data/ConwayPol/index.html or https://github.com/sagemath/conway-polynomials. [66] M. O. Rabin, Probabilistic algorithm for testing primality, Journal of number theory 12 (1980) 128–138. [67] D. Jovanovic, B. Dutertre, Libpoly: A library for reasoning about polynomials, in: Intl. Workshop on Satisfiability
Modulo Theories (SMT), CEUR Workshop Proceedings, 2017. [68] J. Abbott, A. M. Bigatti, Gröbner bases for everyone with CoCoA-5 and CoCoALib, in: The 50th Anniversary of Gröbner Bases, volume 77, Mathematical Society of Japan, 2018, pp. 1–25.