The impossible boomerang attack (IBA) is a combination of the impossible differential attack and boomerang attack, which has demonstrated remarkable power in the security evaluation of AES and other block ciphers. However, this method has not received sufficient attention in the field of symmetric cipher analysis. The only existing search method for impossible boomerang distinguishers (IBD), the core of IBAs, is the $\mathcal{UB}\text{-method}$, but it is considered rather rudimentary given...

LoPher brings, for the first time, cryptographic security promises to the field of logic locking in a bid to break the game of cat-and-mouse seen in logic locking. Toward this end, LoPher embeds the circuitry to lock within multiple rounds of a block cipher, by carefully configuring all the S-Boxes. To realize general Boolean functionalities and to support varying interconnect topologies, LoPher also introduces additional layers of MUXes between S-Boxes and the permutation operations. The...

\ascon is the final winner of the lightweight cryptography standardization competition $(2018-2023)$. In this paper, we focus on preimage attacks against round-reduced \ascon. The preimage attack framework, utilizing the linear structure with the allocating model, was initially proposed by Guo \textit{et al.} at ASIACRYPT 2016 and subsequently improved by Li \textit{et al.} at EUROCRYPT 2019, demonstrating high effectiveness in breaking the preimage resistance of \keccak. In this...

The most crucial but time-consuming task for differential cryptanalysis is to find a differential with a high probability. To tackle this task, we propose a new SAT-based automatic search framework to efficiently figure out a differential with the highest probability under a specified condition. As the previous SAT methods (e.g., the Sun et al’s method proposed at ToSC 2021(1)) focused on accelerating the search for an optimal single differential characteristic, these are not optimized for...

As low-latency designs tend to have a small number of rounds to decrease latency, the differential-type cryptanalysis can become a significant threat to them. In particular, since a multiple-branch-based design, such as Orthros can have the strong clustering effect on differential attacks due to its large internal state, it is crucial to investigate the impact of the clustering effect in such a design. In this paper, we present a new SAT-based automatic search method for evaluating the...

A good differential is a start for a successful differential attack. However, a differential might be invalid, i.e., there is no right pair following the differential, due to some contradictions in the conditions imposed by the differential. This paper presents a novel and handy method for searching and verifying differential trails from an algebraic perspective. From this algebraic perspective, exact Boolean expressions of differentials over a cryptographic primitive can be conveniently...

In this work, we focus on collision attacks against instances of SHA-3 hash family in both classical and quantum settings. Since the 5-round collision attacks on SHA3-256 and other variants proposed by Guo et al. at JoC~2020, no other essential progress has been published. With a thorough investigation, we identify that the challenges of extending such collision attacks on SHA-3 to more rounds lie in the inefficiency of differential trail search. To overcome this obstacle, we develop a...

Firstly, we improve the evaluation theory of differential propagation for modular additions and XORs, respectively. By introducing the concept of $additive$ $sums$ and using signed differences, we can add more information of value propagation to XOR differential propagation to calculate the probabilities of differential characteristics more precisely. Based on our theory, we propose the first modeling method to describe the general ARX differential propagation, which is not based on the...

Existing logic-locking attacks are known to successfully decrypt a functionally correct key of a locked combinational circuit. Extensions of these attacks to real-world Intellectual Properties (IPs, which are sequential circuits) have been demonstrated through the scan-chain by selectively initializing the combinational logic and analyzing the responses. In this paper, we propose SeqL+ to mitigate a broad class of such attacks. The key idea is to lock selective functional-input/scan-output...

Cryptanalysis based on deep learning has become a hotspot in the international cryptography community since it was proposed. The key point of differential cryptanalysis based on deep learning is to find a neural differential distinguisher with longer rounds or higher probability. Therefore it is important to research how to improve the accuracy and the rounds of neural differential distinguisher. In this paper, we design SAT-based algorithms to find a good input difference so that the...

Due to high IC design costs and emergence of countless untrusted foundries, logic encryption has been taken into consideration more than ever. In state-of-the-art logic encryption works, a lot of performance is sold to guarantee security against both the SAT-based and the removal attacks. However, the SAT-based attack cannot decrypt the sequential circuits if the scan chain is protected or if the unreachable states encryption is adopted. Instead, these security schemes can be defeated by the...

Since Keccak was selected as the SHA-3 standard, more and more permutation-based primitives have been proposed. Different from block ciphers, there is no round key in the underlying permutation for permutation-based primitives. Therefore, there is a higher risk for a differential characteristic of the underlying permutation to become incompatible when considering the dependency of difference transitions over different rounds. However, in most of the MILP or SAT based models to search for...

The active participation of external entities in the manufacturing flow has produced numerous hardware security issues in which piracy and overproduction are likely to be the most ubiquitous and expensive ones. The main approach to prevent unauthorized products from functioning is logic encryption that inserts key-controlled gates to the original circuit in a way that the valid behavior of the circuit only happens when the correct key is applied. The challenge for the security designer is to...

Logic locking has emerged as a promising solution against IP piracy and modification by untrusted entities in the integrated circuit design process. However, its security is challenged by boolean satisfiability (SAT) based attacks. Criteria that are critical to SAT attack success on obfuscated circuits includes scan architecture access to the attacker and/or that the circuit under attack is combinational. To address this issue, we propose a dynamically-obfuscated scan chain (DOSC) technique...

Logic encryption, a method to lock a circuit from unauthorized use unless the correct key is provided, is the most important technique in hardware IP protection. However, with the discovery of the SAT attack, all traditional logic encryption algorithms are broken. New algorithms after the SAT attack are all vulnerable to structural analysis unless a provable obfuscation is applied to the locked circuit. But there is no provable logic obfuscation available, in spite of some vague resorting to...

With continuously shrinking feature sizes of integrated circuits, the vast majority of semiconductor companies have become fabless, i.e., chip manufacturing has been outsourced to foundries across the globe. However, by outsourcing critical stages of IC fabrication, the design house puts trust in entities which may have malicious intents. This exposes the design industry to a number of threats, including piracy via unauthorized overproduction and subsequent reselling on the black market. One...

Stripped Function Logic Locking (SFLL) as the most advanced logic locking technique is robust against both the SAT-based and the removal attacks under the assumption of thorough resynthesis of the stripped function. In this paper, we propose a bit-coloring attack based on our discovery of a critical vulnerability in SFLL. In fact, we show that if only one protected input pattern is discovered, then the scheme can be unlocked with a polynomial number of queries to an activated circuit. As a...

Logic encryption is a powerful hardware protection technique that uses extra key inputs to lock a circuit from piracy or unauthorized use. The recent discovery of the SAT-based attack with Distinguishing Input Pattern (DIP) generation has rendered all traditional logic encryptions vulnerable, and thus the creation of new encryption methods. However, a critical question for any new encryption method is whether security against the DIP-generation attack means security against all other...

Logic encryption has attracted much attention due to increasing IC design costs and growing number of untrusted foundries. Unreachable states in a design provide a space of flexibility for logic encryption to explore. However, due to the available access of scan chain, traditional combinational encryption cannot leverage the benefit of such flexibility. Cyclic logic encryption inserts key-controlled feedbacks into the original circuit to prevent piracy and overproduction. Based on our...

Cyclic logic encryption is newly proposed in the area of hardware security. It introduces feedback cycles into the circuit to defeat existing logic decryption techniques. To ensure that the circuit is acyclic under the correct key, CycSAT is developed to add the acyclic condition as a CNF formula to the SAT-based attack. However, we found that it is impossible to capture all cycles in any graph with any set of feedback signals as done in the CycSAT algorithm. In this paper, we propose a...

While financially advantageous, outsourcing key steps such as testing to potentially untrusted Outsourced Semiconductor Assembly and Test (OSAT) companies may pose a risk of compromising on-chip assets. Obfuscation of scan chains is a technique that hides the actual scan data from the untrusted testers; logic inserted between the scan cells, driven by a secret key, hide the transformation functions between the scan- in stimulus (scan-out response) and the delivered scan pattern (captured...

This paper proposes Functional Analysis attacks on state of the art Logic Locking algorithms (abbreviated as FALL attacks). FALL attacks have two stages. The first stage identifies nodes involved in the locking functionality and analyzes functional properties of these nodes to shortlist a small number of candidate locking keys. In many cases, this shortlists exactly one locking key, so no further analysis is needed. However, if more than one key is shortlisted, the second stage introduces a...

When designing a new symmetric-key primitive, the designer must show resistance to known attacks. Perhaps most prominent amongst these are linear and differential cryptanalysis. However, it is notoriously difficult to accurately demonstrate e.g. a block cipher's resistance to these attacks, and thus most designers resort to deriving bounds on the linear correlations and differential probabilities of their design. On the other side of the spectrum, the cryptanalyst is interested in...

Logic encryption is a hardware security technique that uses extra key inputs to prevent unauthorized use of a circuit. With the discovery of the SAT-based attack, new encryption techniques such as SARLock and Anti-SAT are proposed, and further combined with traditional logic encryption techniques, to guarantee both high error rates and resilience to the SAT-based attack. In this paper, the SAT-based bit-flipping attack is presented. It first separates the two groups of keys via SAT-based...

Logic encryption is an important hardware protection technique that adds extra keys to lock a given circuit. With recent discovery of the effective SAT-based attack, new enhancement methods such as SARLock and Anti-SAT have been proposed to thwart the SAT-based and similar exact attacks. Since these new techniques all have very low error rate, approximate attacks such as Double DIP and AppSAT have been proposed to find an almost correct key with low error rate. However, measuring the...

Logic encryption is an important hardware security technique that introduces keys to modify a given combinational circuit in order to lock the functionality from unauthorized uses. Traditional methods are all ad hoc approaches based on inserting lock gates with keys on randomly selected signals in the original circuit. Thus, it was not a surprise that a SAT-based attack developed by Subramanyan et al. successfully defeated almost all of them. New approaches such as SARLock and Anti-SAT were...

Cyclic logic encryption is a newly proposed circuit obfuscation technique in hardware security. It was claimed to be SAT-unresolvable because feedback cycles were intentionally inserted under keys into the encryption. We show in the paper that even though feedback cycles introduce extra difficulty for an attacker, they can still be overcome with SAT- based techniques. Specifically, we propose CycSAT Algorithms based on SAT with different acyclic conditions that can efficiently decrypt cyclic...

With the adoption of a globalized and distributed IC design flow, IP piracy, reverse engineering, and counterfeiting threats are becoming more prevalent. Logic obfuscation techniques including logic locking and IC camouflaging have been developed to address these emergent challenges. A major challenge for logic locking and camouflaging techniques is to resist Boolean satisfiability (SAT) based attacks that can circumvent state-of-the-art solutions within minutes. Over the past year, multiple...

Logic encryption is a hardware security technique that uses extra key inputs to lock a given combinational circuit. A recent study by Subramanyan et al. shows that all existing logic encryption techniques can be successfully attacked. As a countermeasure, SARLock was proposed to enhance the security of existing logic encryptions. In this paper, we re- evaluate the security of these approaches. A SAT-based at- tack called Double DIP is proposed and shown to success- fully defeat...

We show how short cycles in the state space of a cryptographic algorithm can be used to mount a fault attack on its implementation which results in a full secret key recovery. The attack is based on the assumption that an attacker can inject a transient fault at a precise location and time of his/her choice and more than once. We present an algorithm which uses a SAT-based bounded model checking for finding all short cycles of a given length. The existing Boolean Decision Diagram (BDD) based...

We investigate six authenticated encryption schemes (ACORN, ASCON-128a, Ketje Jr, ICEPOLE-128a, MORUS, and NORX-32) from the CAESAR competition. We aim at state recovery attacks using a SAT solver as a main tool. Our analysis reveals that these schemes, as submitted to CAESAR, provide strong resistance against SAT-based state recoveries. To shed a light on their security margins, we also analyse modified versions of these algorithms, including round-reduced variants and versions with higher...

Logic encryption protects integrated circuits (ICs) against intellectual property (IP) piracy and over- building attacks by encrypting the IC with a key. A Boolean satisfiability (SAT) based attack breaks all existing logic encryption technique within few hours. Recently, a defense mechanism known as Anti-SAT was presented that protects against SAT attack, by rendering the SAT-attack effort exponential in terms of the number of key gates. In this paper, we highlight the vulnerabilities of...

Over the last decade, hardware Trojans have gained increasing attention in academia, industry and by government agencies. In order to design reliable countermeasures, it is crucial to understand how hardware Trojans can be built in practice. This is an area that has received relatively scant treatment in the literature. In this contribution, we examine how particularly stealthy Trojans can be introduced to a given target circuit. The Trojans are triggered by violating the delays of very rare...

Logic locking is a technique that has been proposed to protect outsourced IC designs from piracy and counterfeiting by untrusted foundries. It can hide the functionality of an IC by inserting key-controlled logic gates into the original design. The locked IC preserves the correct functionality only when a correct key is provided. Recently, the security of logic locking is threatened by a new type of attack called satisfiability checking (SAT) based attack, which can decipher the correct key...

The CAESAR competition aims to provide a portfolio of authenticated encryption algorithms. SAT solvers represent powerful tools to verify automatically and efficiently (among others) the confidentiality and the authenticity of information claimed by cryptographic primitives. In this work, we study the security of the CAESAR candidate ACORN against a SAT-based cryptanalysis. We provide the first practical and efficient attacks on the first and the last versions of ACORN. More precisely, we...

NXP Semiconductors and its academic partners challenged the cryptographic community with finding practical attacks on the block cipher they designed, PRINCE. Instead of trying to attack as many rounds as possible using attacks which are usually impractical despite being faster than brute-force, the challenge invites cryptographers to find practical attacks and encourages them to actually implement them. In this paper, we present new attacks on round-reduced PRINCE including the ones which...

In order to obtain differential patterns over many rounds of a cryptographic primitive, the cryptanalyst often needs to work on local differential trail analysis. Examples include merging two differential trail parts into one or, in the case of boomerang and rectangle attacks, connecting two short trails within the quartet boomerang setting. In the latter case, as shown by Murphy in 2011, caution should be exercised as there is increased chance of running into contradictions in the middle...

In 2007, the U.S. National Institute of Standards and Technology (NIST) announced a public contest aiming at the selection of a new standard for a cryptographic hash function. In this paper, the security margin of five SHA-3 finalists is evaluated with an assumption that attacks launched on finalists should be practically verified. A method of attacks applied is called logical cryptanalysis where the original task is expressed as a SATisfiability problem instance. A new toolkit is used to...

In this paper, we present a preimage attack on reduced versions of Keccak hash functions. We use our recently developed toolkit CryptLogVer for generating CNF (conjunctive normal form) which is passed to the SAT solver PrecoSAT. We found preimages for some reduced versions of the function and showed that full Keccak function is secure against the presented attack.