International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News

Updates on the COVID-19 situation are on the Announcement channel.

Here you can see all recent updates to the IACR webpage. These updates are also available:

RSS symbol icon
via RSS feed
Twitter bird icon
via Twitter
Weibo icon
via Weibo
Facebook icon
via Facebook

31 July 2024

Xavier Bonnetain, Virginie Lallemand
ePrint Report ePrint Report
In this short note we examine one of the impossible boomerang distinguishers of Skinny-128-384 provided by Zhang, Wang and Tang at ToSC 2024 Issue 2 and disprove it.

The issue arises from the use of the Double Boomerang Connectivity Table (DBCT) as a tool to establish that a boomerang switch over 2 rounds has probability zero, whereas the DBCT only covers specific cases of difference propagation, missing a large set of events that might make the connection possible.

We study in details the specific instance provided by Zhang et al. and display one example of a returning quartet that contradicts the impossibility.
Expand
Jong-Yeon Park, Wonil Lee, Bo Gyeong Kang, Il-jong Song, Jaekeun Oh, Kouichi Sakurai
ePrint Report ePrint Report
A prominent countermeasure against side channel attacks, the hiding countermeasure, typically involves shuffling operations using a permutation algorithm. Especially in the era of Post-Quantum Cryptography, the importance of the hiding coun- termeasure is emphasized due to computational characteristics like those of lattice and code-based cryptography. In this context, swiftly and securely generating permutations has a critical impact on an algorithm’s security and efficiency. The widely adopted Fisher-Yates shuffle, because of its high security and ease of implementation, is prevalent. However, it has a limitation of complexity O(?) due to its sequential nature. In response, we propose a time-area trade-off swap algorithm, FSS, based on the Butterfly Network with only log(?) depth, log(?) works and O(1) operation time in parallel. We will calculate the maximum gain that an attacker can achieve through butterfly operations with only log(?) depth from side channel analysis perspective. In particular, we will show that it is possible to derive a generalized formula of the attack complexity with higher-order side channel attacks for arbitrary input sizes through a fractal structure of the butterfly network. Furthermore, our research highlights the possibility of generating efficient and secure permutations utilizing a minimal amount of randomness.
Expand
Scott Griffy, Anna Lysyanskaya, Omid Mir, Octavio Perez Kempner, Daniel Slamanig
ePrint Report ePrint Report
Delegatable anonymous credentials (DACs) are anonymous credentials that allow a root issuer to delegate their credential-issuing power to secondary issuers who, in turn, can delegate further. This delegation, as well as credential showing, is carried out in a privacy-preserving manner, so that credential recipients and verifiers learn nothing about the issuers on the delegation chain. One particularly efficient approach to constructing DACs is due to Crites and Lysyanskaya (CT-RSA'19), based on mercurial signatures, which is a type of equivalence-class signatures. In contrast to previous approaches, this design is conceptually simple and does not require extensive use of non-interactive zero-knowledge proofs. Unfortunately, the ``CL-type'' DAC schemes proposed so far have a privacy limitation: if an adversarial issuer (even an honest-but-curious one) was part of an honest user's delegation chain, the adversary will be able to detect this fact (and identify the specific adversarial issuer) when an honest user shows its credential. This is because underlying mercurial signature schemes allow the owner of a secret key to detect when his key was used in a delegation chain.

In this paper we show that it is possible to construct CL-type DACs that does not suffer from this privacy issue. We give a new mercurial signature scheme that provides adversarial public key class hiding; i.e. even if an adversarial signer participated in the delegation chain, the adversary won't be able to identify this fact. This is achieved by introducing structured public parameters which for each delegation level, enabling strong privacy features in DAC. Since the setup of these parameters also produces trapdoors that are problematic in privacy applications, we show how to overcome this problem by using techniques from updatable structured reference string in zero-knowledge proof systems (Groth et al. CRYPTO'18).

In addition, we propose a simple way to realize revocation for CL-type DACs via the concept of revocation tokens. While we showcase this approach to revocation using our DAC scheme, it is generic and can be applied to any CL-type DAC system. Revocation is a feature that is largely unexplored and notoriously hard to achieve for DACs. However as it is a vital feature for any anonymous credential system, this can help to make DAC schemes more attractive for practical applications.
Expand
Chris Brzuska, Cas Cremers, Håkon Jacobsen, Douglas Stebila, Bogdan Warinschi
ePrint Report ePrint Report
A security proof for a key exchange protocol requires writing down a security definition. Authors typically have a clear idea of the level of security they aim to achieve. Defining the model formally additionally requires making choices on games vs. simulation-based models, partnering, on having one or more Test queries and on adopting a style of avoiding trivial attacks: exclusion, penalizing or filtering. We elucidate the consequences, advantages and disadvantages of the different possible model choices. Concretely, we show that a model with multiple Test queries composes tightly with symmetric-key protocols while models with a single Test query require a hybrid argument that loses a factor in the number of sessions. To illustrate the usefulness of models with multiple Test queries, we prove the Naxos protocol security in said model and obtain a tighter bound than adding a hybrid argument on top of a proof in a single Test query model.

Our composition model exposes partnering information to the adversary, circumventing a previous result by Brzuska, Fischlin, Warinschi, and Williams (CCS 2011) showing that the protocol needs to provide public partnering. Moreover, our baseline theorem of key exchange partnering shows that partnering by key equality provides a joint baseline for most known partnering mechanisms, countering previous criticism by Li and Schäge (CCS 2017) that security in models with existential quantification over session identifiers is non-falsifiable.
Expand
Jiawei Zhang, Jiangshan Long, Changhai Ou, Kexin Qiao, Fan Zhang, Shi Yan
ePrint Report ePrint Report
By introducing collision information, the existing side-channel Correlation-Enhanced Collision Attacks (CECAs) performed collision-chain detection, and reduced a given candidate space to a significantly smaller collision-chain space, leading to more efficient key recovery. However, they are still limited by low collision detection speed and low success rate of key recovery. To address these issues, we first give a Collision Detection framework with Genetic Algorithm (CDGA), which exploits Genetic Algorithm to detect the collision chains and has a strong capability of global searching. Secondly, we theoretically analyze the performance of CECA, and bound the searching depth of its output candidate vectors with a confidence level using a rigorous hypothesis test, which is suitable both for Gaussian and non-Gaussian leakages. This facilitates the initialization of the population. Thirdly, we design an innovative goal-directed mutation method to randomly select new gene values for replacement, thus improving efficiency and adaptability of the CDGA. Finally, to optimize the evolutionary of CDGA, we introduce roulette selection strategy to employ a probability assignment based on individual fitness values to guarantee the preferential selection of superior genes. A single-point crossover strategy is also used to introduce novel gene segments into the chromosomes, thus enhancing the genetic diversity of the population. Experiments verify the superiority of our CDGA.
Expand
NXP Semiconductors Austria GmbH & CO KG
Job Posting Job Posting
Ready to join the future of innovation in our team at NXP in Gratkorn/Graz? Owing to the success of our business, our department is growing and we are looking for a talented student, who would like to gain experience in parallel to their studies. In this exciting role, you will be part of a highly talented team developing secure high performance crypto software for next generation products in different market segments (payment, identification, mobile, IoT, Automotive, …)

Your responsibilities:
  • Supporting the Crypto Library development and maintenance
  • Embedded software development in C
  • Implementation of cryptographic algorithms
  • Maintenance of quality KPIs

    Your profile:
  • Ongoing studies in mathematics, computer science, electronic/ electrical engineering, information technology or similar
  • First experience in embedded software development, using C and assembly is an advantage
  • A solid understanding of microcontroller architecture
  • First experience in implementing crypto algorithms such as DES, AES, RSA, ECC, SHA is appreciated
  • You are a team player and you have initiative
  • Availability around 16 hours per week (on average)
  • The minimum salary for this position is EUR 17 gross/hour.

    We offer:
  • Flexible working time
  • On-site free beverages and fresh fruit
  • Social events (student get-togethers, networking opportunities, etc)
  • and many other benefits!
  • We offer internships with a variety of lengths.

    We are proud to have received the Leading Employer Award for the 5th time in a row 2023, which is presented exclusively only to the top 1% of employers in Austria. Furthermore, we have recently been certified as Family Friendly Employer and received the EqualitA label.

    Closing date for applications:

    Contact: Laura Hoser

    More information: https://nxp.wd3.myworkdayjobs.com/careers/job/Gratkorn/Internship--Crypto-Library-SW-Development--f-m-d-_R-10053816

  • Expand
    Rovira i Virgili University, Tarragona, Spain
    Job Posting Job Posting
    We seek to hire an outstanding PhD candidate to start in December 2024. The successful candidate will participate in the activities of the CRISES research group, which focuses on theoretical advances for computer security and data privacy.

    The University offers:
  • A 4-year PhD scholarship to work in an exciting international environment located at the sunny and mediterranean city of Tarragona, Spain.
  • Generous travel funds for participation in conferences, summer schools, and research stays.
  • An automatic switch to a postdoctoral contract once the candidate defends the PhD thesis.
  • Profile:
  • A First Class Honours degree (or equivalent) or Master degree (with research component) in computer science or mathematics
  • Strong academic performance, programming and mathematical skills
  • A proven interest in computer security and/or related topics
  • Excellent written and oral English skills
  • Commitment, team worker, self-motivated and a critical mind
  • Applications should be written in English and include the following documents:
  • Curriculum Vitae
  • A short description of your Master work or Honours thesis (max 1 page)
  • Transcript of grades from all university-level courses taken
  • Contact information for 3 referees
  • Closing date for applications:

    Contact: Dr. Rolando Trujillo rolando.trujillo@urv.cat

    More information: https://rolandotr.bitbucket.io/open-positions.html

    Expand
    University of South Florida, The Department of Computer Science and Engineering, Tampa, FL, USA.
    Job Posting Job Posting
    We have a fully funded Ph.D. position about Deep Learning (DL) and secure multi-party computation (MPC) applied to medical systems beginning from Fall 2025 (August 2025) or Spring 2025 (January 2025) at University of South Florida (USF). Students receive a yearly package worth approximately $65,000, which covers all the tuition, health insurance, fringe benefits, and a competitive monthly salary. The project offers an excellent multi-disciplinary opportunity involving flagship medical centers, and top machine learning experts, all with MPC and applied cryptography. The candidate will work on private diagnosis with DL and federated learning, developing specially designed MPC protocols for medical applications. USF is a Rank-1 Research University, AAU University, and USF CSE is in the top 15% among Computer Science departments in public universities based on Academic Analytics data based on Scholarly Research Index (and top 8th for patents in the USA). Requirements:
    • A BS degree in ECE/CS with a high GPA
    • Excellent programming skills (e.g., C, C++), familiarity with Linux
    • MS degree in ECE/CS/Math is a big plus. Publications will be regarded as a plus but not required.
    • Please send your CV, transcripts, TOEFL/IELTS scores (required), publications (optional), and GRE (highly preferred).
    • Closing date for applications:

      Contact:
      Email: attilaayavuz@usf.edu
      Webpage : http://www.csee.usf.edu/~attilaayavuz/

    Expand

    29 July 2024

    Kaartik Bhushan, Alexis Korb, Amit Sahai
    ePrint Report ePrint Report
    Streaming functional encryption (sFE), recently introduced by Guan, Korb, and Sahai [Crypto 2023], is an extension of functional encryption (FE) tailored for iterative computation on dynamic data streams. Unlike in regular FE, in an sFE scheme, users can encrypt and compute on the data as soon as it becomes available and in time proportional to just the size of the newly arrived data.

    As sFE implies regular FE, all known constructions of sFE and FE for $\mathsf{P/Poly}$ require strong cryptographic assumptions which are powerful enough to build indistinguishability obfuscation. In contrast, bounded-collusion FE, in which the adversary is restricted to making at most $Q$ function queries for some polynomial $Q$ determined at setup, can be built from the minimal assumptions of public-key encryption (for public-key FE) [Sahai and Seyalioglu, CCS 2010; Gorbunov, Vaikuntanathan, and Wee, CRYPTO 2012] and secret-key encryption (for secret-key FE)[Ananth, Vaikuntanathan, TCC 2019].

    In this paper, we introduce and build bounded-collusion streaming FE for any polynomial bound $Q$ from the same minimal assumptions of public-key encryption (for public-key sFE) and secret-key encryption (for secret-key sFE). Similarly to the original sFE paper of Guan, Korb, and Sahai, our scheme satisfies semi-adaptive-function-selective security which is similar to standard adaptive indistinguishability-based security except that we require all functions to be queried before any of the challenge messages.

    Along the way, our work also replaces a key ingredient (called $\mathsf{One}\text{-}\mathsf{sFE}$) from the original work of Guan, Korb, and Sahai with a much simpler construction based on garbled circuits.
    Expand
    CHANGCHANG DING, Zheming Fu
    ePrint Report ePrint Report
    We present an efficient layered circuit design for SHA3-256 Merkle tree verification, suitable for a GKR proof system, that achieves logarithmic verification and proof size. We demonstrate how to compute the predicate functions for our circuit in $O(\log n)$ time to ensure logarithmic verification and provide GKR benchmarks for our circuit.
    Expand
    Julius Hermelink, Silvan Streit, Erik Mårtensson, Richard Petri
    ePrint Report ePrint Report
    Lattice-based cryptography is in the process of being standardized. Several proposals to deal with side-channel information using lattice reduction exist. However, it has been shown that algorithms based on Bayesian updating are often more favorable in practice.

    In this work, we define distribution hints; a type of hint that allows modelling probabilistic information. These hints generalize most previously defined hints and the information obtained in several attacks.

    We define two solvers for our hints; one is based on belief propagation and the other one uses a greedy approach. We prove that the latter is a computationally less expensive approximation of the former and that previous algorithms used for specific attacks may be seen as special cases of our solvers. Thereby, we provide a systematization of previously obtained information and used algorithms in real-world side-channel attacks.

    In contrast to lattice-based approaches, our framework is not limited to value leakage. For example, it can deal with noisy Hamming weight leakage or partially incorrect information. Moreover, it improves upon the recovery of the secret key from approximate hints in the form they arise in real-world attacks. Our framework has several practical applications: We exemplarily show that a recent attack can be improved; we reduce the number of traces and corresponding ciphertexts and increase the noise resistance. Further, we explain how distribution hints could be applied in the context of previous attacks and outline a potential new attack.
    Expand
    Quang Dao, Justin Thaler
    ePrint Report ePrint Report
    Many fast SNARKs apply the sum-check protocol to an $n$-variate polynomial of the form $g(x) = \text{eq}(w,x) \cdot p(x)$, where $p$ is a product of multilinear polynomials, $w \in \mathbb{F}^n$ is a random vector, and $\text{eq}$ is the multilinear extension of the equality function.

    In this setting, we describe an optimization to the sum-check prover that substantially reduces the cost coming from the $\text{eq}(w, x)$ factor. Our work further improves on a prior optimization by Gruen (ePrint 2023), and in the small-field case, can be combined with additional optimizations by Bagad, Domb, and Thaler (ePrint 2024), and Dao and Thaler (ePrint 2024).

    Over large prime-order fields, our optimization eliminates roughly $2^{n + 1}$ field multiplications compared to a standard linear-time implementation of the prover, and roughly $2^{n-1}$ field multiplications when considered on top of Gruen's optimization. These savings are about a 25% (respectively 10%) end-to-end prover speedup in common use cases, and potentially even larger when working over binary tower fields.
    Expand
    Mohammed Alghazwi, Tariq Bontekoe, Leon Visscher, Fatih Turkmen
    ePrint Report ePrint Report
    Non-interactive zero-knowledge (NIZK) proofs of knowledge have proven to be highly relevant for securely realizing a wide array of applications that rely on both privacy and correctness. They enable a prover to convince any party of the correctness of a public statement for a secret witness. However, most NIZKs do not natively support proving knowledge of a secret witness that is distributed over multiple provers. Previously, collaborative proofs [51] have been proposed to overcome this limitation. We investigate the notion of composability in this setting, following the Commit-and-Prove design of LegoSNARK [17]. Composability allows users to combine different, specialized NIZKs (e.g., one arithmetic circuit, one boolean circuit, and one for range proofs) with the aim of reducing the prove generation time. Moreover, it opens the door to efficient realizations of many applications in the collaborative setting such as mutually exclusive prover groups, combining collaborative and single-party proofs and efficiently implementing publicly auditable MPC (PA-MPC).

    We present the first, general definition for collaborative commit-and-prove NIZK (CP-NIZK) proofs of knowledge and construct distributed protocols to enable their realization. We implement our protocols for two commonly used NIZKs, Groth16 and Bulletproofs, and evaluate their practicality in a variety of computational settings. Our findings indicate that composability adds only minor overhead, especially for large circuits. We experimented with our construction in an application setting, and when compared to prior works, our protocols reduce latency by 18–55× while requiring only a fraction (0.2%) of the communication.
    Expand
    Michael Rosenberg, Tushar Mopuri, Hossein Hafezi, Ian Miers, Pratyush Mishra
    ePrint Report ePrint Report
    Zero-knowledge Succinct Non-interactive ARguments of Knowledge (zkSNARKs) allow a prover to convince a verifier of the correct execution of a large computation in private and easily-verifiable manner. These properties make zkSNARKs a powerful tool for adding accountability, scalability, and privacy to numerous systems such as blockchains and verifiable key directories. Unfortunately, existing zkSNARKs are unable to scale to large computations due to time and space complexity requirements for the prover algorithm. As a result, they cannot handle real-world instances of the aforementioned applications. In this work, we introduce Hᴇᴋᴀᴛᴏɴ, a zkSNARK that overcomes these barriers and can efficiently handle arbitrarily large computations. We construct Hᴇᴋᴀᴛᴏɴ via a new "distribute-and-aggregate" framework that breaks up large computations into small chunks, proves these chunks in parallel in a distributed system, and then aggregates the resulting chunk proofs into a single succinct proof. Underlying this framework is a new technique for efficiently handling data that is shared between chunks that we believe could be of independent interest. We implement a distributed prover for Hᴇᴋᴀᴛᴏɴ, and evaluate its performance on a compute cluster. Our experiments show that Hᴇᴋᴀᴛᴏɴ achieves strong horizontal scalability (proving time decreases linearly as we increase the number of nodes in the cluster), and is able to prove large computations quickly: it can prove computations of size $2^{35}$ gates in under an hour, which is much faster than prior work.

    Finally, we also apply Hᴇᴋᴀᴛᴏɴ to two applications of real-world interest: proofs of batched insertion for a verifiable key directory and proving correctness of RAM computations. In both cases, Hᴇᴋᴀᴛᴏɴ is able to scale to handle realistic workloads with better efficiency than prior work.
    Expand
    Michael Walter
    ePrint Report ePrint Report
    In recent years, there have been several constructions combining FHE with SNARGs to add integrity guarantees to FHE schemes. Most of these works focused on improving efficiency, while the precise security model with regards to client side input privacy has remained understudied. Only recently it was shown by Manulis and Nguyen (Eurocrypt'24) that this combination does not yield IND-CCA1 security. So an interesting open question is: does the SNARG actually add any meaningful security to input privacy? We address this question in this note and give a security definition that meaningfully captures the security of the FHE plus SNARG construction.
    Expand
    Daniel de Haro Moraes, Joao Paulo Aragao Pereira, Bruno Estolano Grossi, Gustavo Mirapalheta, George Marcel Monteiro Arcuri Smetana, Wesley Rodrigues, Courtnay Nery Guimarães Jr., Bruno Domingues ...
    ePrint Report ePrint Report
    This article presents an innovative project for a Central Bank Digital Currency (CBDC) infrastructure. Focusing on security and reliability, the proposed architecture: (1) employs post-quantum cryptography (PQC) algorithms for long-term security, even against attackers with access to cryptographically-relevant quantum computers; (2) can be integrated with a Trusted Execution Environment (TEE) to safeguard the confidentiality of transaction contents as they are processed by third-parties; and (3) uses Distributed Ledger Technology (DLT) to promote a high level of transparency and tamper resistance for all transactions registered in the system. Besides providing a theoretical discussion on the benefits of this architecture, we experimentally evaluate its components. Namely, as PQC algorithms, we consider three signature schemes being standardized by the National Institute of Standards and Technology (NIST), CRYSTALS-Dilithium, Falcon, and SPHINCS+. Those algorithms are integrated into the Hyperledger Besu (DLT) and executed both inside and outside an Intel SGX TEE environment. According to our results, CRYSTALS-Dilithium-2 combined with classical secp256k1 signatures leads to the shortest execution times when signing blocks in the DLT, reaching 1.68ms without the TEE, and 2.09ms with TEE. The same combination also displays the best results for signature verifications, achieving 0.5ms without a TEE and 1.98ms with a TEE. We also describe the main aspects of the evaluation methodology and the next steps in validating the proposed infrastructure. The conclusions drawn from our experiments is that the combination of PQC and TEE promises highly secure and effective DLT-based CBDC scenarios, ready to face the challenges of the digital financial future and potential quantum threats.
    Expand
    Zhengjun Cao, Lihua Liu
    ePrint Report ePrint Report
    We show that the Chunka-Banerjee-Goswami authentication and key agreement scheme [Wirel. Pers. Commun., 117, 1361-1385, 2021] fails to keep user anonymity, not as claimed. It only keeps pseudonymity. Anonymous actions are designed to be unlinkable to any entity, but pseudonymous actions can be traced back to a certain entity. We also find the scheme is insecure against offline dictionary attack.
    Expand
    Sergiu Carpov
    ePrint Report ePrint Report
    Functional bootstrapping in FHE schemes such as FHEW and TFHE allows the evaluation of a function on an encrypted message, in addition to noise reduction. Implementing programs that directly use functional bootstrapping is challenging and error-prone. In this paper, we propose a heuristic that automatically maps Boolean circuits to functional bootstrapping instructions. Unlike other approaches, our method does not limit the encrypted data plaintext space to a power-of-two size, allowing the instantiation of functional bootstrapping with smaller parameters. Furthermore, the negacyclic property of functional bootstrapping is exploited to extend the plaintext space. Despite the inherently greedy nature of the heuristic, experimental results show that the mapped circuits exhibit a significant reduction in evaluation time. Furthermore, our heuristic was able to achieve a $45\%$ improvement in evaluation time when applied to manually implemented Trivium and Kreyvium circuits.
    Expand
    Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
    ePrint Report ePrint Report
    Compilers often weaken or even discard software-based countermeasures commonly used to protect programs against side-channel attacks; worse, they may also introduce vulnerabilities that attackers can exploit. The solution to this problem is to develop compilers that preserve these countermeasures. Prior work establishes that (a mildly modified version of) the CompCert and Jasmin formally verified compilers preserve constant-time, an information flow policy that ensures that programs are protected against cache side-channel attacks. However, nothing is known about preservation of speculative constant-time, a strengthening of the constant-time policy that ensures that programs are protected against Spectre v1 attacks. We first show that preservation of speculative constant-time fails in practice by providing examples of secure programs whose compilation is not speculative constant-time using GCC (GCC -O0 and GCC -O1) and Jasmin. Then, we define a proof-of-concept compiler that distills some of the critical passes of the Jasmin compiler and use the Coq proof assistant to prove that it preserves speculative constant-time. Finally, we patch the Jasmin speculative constant-time type checker and demonstrate that all cryptographic implementations written in Jasmin can be fixed with minimal impact.
    Expand
    Feng Zhou, Hua Chen, Limin Fan
    ePrint Report ePrint Report
    In recent years, formal verification has emerged as a crucial method for assessing security against Side-Channel attacks of masked implementations, owing to its remarkable versatility and high degree of automation. However, formal verification still faces technical bottlenecks in balancing accuracy and efficiency, thereby limiting its scalability. Former efficient tools like \textsf{maskVerif} and CocoAlma are often inaccurate when verifying schemes utilizing properties of Boolean functions. Later, SILVER addressed the accuracy issue, albeit at the cost of significantly reduced speed and scalability compared to \textsf{maskVerif}. Consequently, there is a pressing need to develop formal verification tools that are both efficient and accurate for designing secure schemes and evaluating implementations. This paper's primary contribution lies in proposing several approaches to develop a more efficient and scalable formal verification tool called \textsf{Prover}, which is built upon SILVER. Firstly, inspired by the auxiliary data structures proposed by Eldib et al. and optimistic sampling rule of maskVerif, we introduce two reduction rules aimed at diminishing the size of observable sets and secret sets in statistical independence checks. These rules substantially decrease, or even eliminate, the need for repeated computation of probability distributions using Reduced Ordered Binary Decision Diagrams (ROBDDs), a time-intensive procedure in verification. Subsequently, we integrate one of these reduction rules into the uniformity check to mitigate its complexity. Secondly, we identify that variable ordering significantly impacts efficiency and optimize it for constructing ROBDDs, resulting in much smaller representations of investigated functions. Lastly, we present the algorithm of \textsf{Prover}, which efficiently verifies the security and uniformity of masked implementations in probing model with or without the presence of glitches. Experimental results demonstrate that our proposed tool \textsf{Prover} offers a superior balance between efficiency and accuracy compared to other state-of-the-art tools (CocoAlma, maskVerif, and SILVER). It successfully verifies a design that SILVER could not complete within the allocated time, whereas CocoAlma and maskVerif encounter issues with false positives.
    Expand
    ◄ Previous Next ►