-
Implementation of Entropically Secure Encryption: Securing Personal Health Data
Authors:
Mehmet Hüseyin Temel,
Boris Skoric,
Idelfonso Tafur Monroy
Abstract:
Entropically Secure Encryption (ESE) offers unconditional security with shorter keys compared to the One-Time Pad. In this paper, we present the first implementation of ESE for bulk encryption. The main computational bottleneck for bulk ESE is a multiplication in a very large finite field. This involves multiplication of polynomials followed by modular reduction. We have implemented polynomial mul…
▽ More
Entropically Secure Encryption (ESE) offers unconditional security with shorter keys compared to the One-Time Pad. In this paper, we present the first implementation of ESE for bulk encryption. The main computational bottleneck for bulk ESE is a multiplication in a very large finite field. This involves multiplication of polynomials followed by modular reduction. We have implemented polynomial multiplication based on the gf2x library, with some modifications that avoid inputs of vastly different length, thus improving speed. Additionally, we have implemented a recently proposed efficient reduction algorithm that works for any polynomial degree. We investigate two use cases: X-ray images of patients and human genome data. We conduct entropy estimation using compression methods whose results determine the key lengths required for ESE. We report running times for all steps of the encryption. We discuss the potential of ESE to be used in conjunction with Quantum Key Distribution (QKD), in order to achieve full information-theoretic security of QKD-protected links for these use cases.
△ Less
Submitted 4 April, 2024;
originally announced April 2024.
-
On the Systematic Creation of Faithfully Rounded Commutative Truncated Booth Multipliers
Authors:
Theo Drane,
Samuel Coward,
Mertcan Temel,
Joe Leslie-Hurd
Abstract:
In many instances of fixed-point multiplication, a full precision result is not required. Instead it is sufficient to return a faithfully rounded result. Faithful rounding permits the machine representable number either immediately above or below the full precision result, if the latter is not exactly representable. Multipliers which take full advantage of this freedom can be implemented using les…
▽ More
In many instances of fixed-point multiplication, a full precision result is not required. Instead it is sufficient to return a faithfully rounded result. Faithful rounding permits the machine representable number either immediately above or below the full precision result, if the latter is not exactly representable. Multipliers which take full advantage of this freedom can be implemented using less circuit area and consuming less power. The most common implementations internally truncate the partial product array. However, truncation applied to the most common of multiplier architectures, namely Booth architectures, results in non-commutative implementations. The industrial adoption of truncated multipliers is limited by the absence of formal verification of such implementations, since exhaustive simulation is typically infeasible. We present a commutative truncated Booth multiplier architecture and derive closed form necessary and sufficient conditions for faithful rounding. We also provide the bit-vectors giving rise to the worst-case error. We present a formal verification methodology based on ACL2 which scales up to 42 bit multipliers. We synthesize a range of commutative faithfully rounded multipliers and show that truncated booth implementations are up to 31% smaller than externally truncated multipliers.
△ Less
Submitted 22 April, 2024;
originally announced April 2024.
-
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2
Authors:
Mertcan Temel
Abstract:
Automatic and efficient verification of multiplier designs, especially through a provably correct method, is a difficult problem. We show how to utilize a theorem prover, ACL2, to implement an efficient rewriting algorithm for multiplier design verification. Through a basic understanding of the features and data structures of ACL2, we created a verified program that can automatically verify vari…
▽ More
Automatic and efficient verification of multiplier designs, especially through a provably correct method, is a difficult problem. We show how to utilize a theorem prover, ACL2, to implement an efficient rewriting algorithm for multiplier design verification. Through a basic understanding of the features and data structures of ACL2, we created a verified program that can automatically verify various multiplier designs much faster than the other state-of-the-art tools. Additionally, users of our system have the flexibility to change the specification for the target design to verify variations of multipliers. We discuss the challenges we tackled during the development of this program as well as key implementation details for efficiency and verifiability. Those who plan to implement an efficient program on a theorem prover or those who wish to implement our multiplier verification methodology on a different system may benefit from the discussions in this paper.
△ Less
Submitted 23 May, 2022;
originally announced May 2022.
-
Entropically secure encryption with faster key expansion
Authors:
Mehmet Huseyin Temel,
Boris Skoric
Abstract:
Entropically secure encryption is a way to encrypt a large plaintext with a small key and still have information-theoretic security, thus in a certain sense circumventing Shannon's result that perfect encryption requires the key to be at least as long as the entropy of the plaintext. Entropically secure encryption is not perfect, and it works only if a lower bound is known on the entropy of the pl…
▽ More
Entropically secure encryption is a way to encrypt a large plaintext with a small key and still have information-theoretic security, thus in a certain sense circumventing Shannon's result that perfect encryption requires the key to be at least as long as the entropy of the plaintext. Entropically secure encryption is not perfect, and it works only if a lower bound is known on the entropy of the plaintext. The typical implementation is to expand the short key to the size of the plaintext, e.g. by multiplication with a public random string, and then use one-time pad encryption. This works in the classical as well as the quantum setting. In this paper, we introduce a new key expansion method that is faster than existing ones. We prove that it achieves the same security. The speed gain is most notable when the key length is a sizeable fraction of the message length. In particular, a factor of 2 is gained in the case of approximate randomization of quantum states.
△ Less
Submitted 23 October, 2022; v1 submitted 1 January, 2022;
originally announced January 2022.
-
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2
Authors:
Mertcan Temel
Abstract:
RP-Rewriter (Retain-Property) is a verified clause processor that can use some of the existing ACL2 rewrite rules to prove conjectures through term rewriting. Optimized for conjectures that can expand into large terms, the rewriter tries to mimic some of the ACL2 rewriting heuristics but also adds some extra features. It can attach side-conditions to terms that help…
▽ More
RP-Rewriter (Retain-Property) is a verified clause processor that can use some of the existing ACL2 rewrite rules to prove conjectures through term rewriting. Optimized for conjectures that can expand into large terms, the rewriter tries to mimic some of the ACL2 rewriting heuristics but also adds some extra features. It can attach side-conditions to terms that help the rewriter retain properties about them and prevent possibly some very expensive backchaining. The rewriter supports user-defined complex meta rules that can return a special structure to prevent redundant rewriting. Additionally, it can store fast alists even when values are not quoted. RP-Rewriter is utilized for two applications, multiplier design proofs and SVEX simplification, which involve very large terms.
△ Less
Submitted 29 September, 2020;
originally announced September 2020.
