Provable security and other problems in modern cryptography
Step 6: Security Analysis of the Implementation
The sixth and last step calls for security evaluation of the concrete instantiation. This is required because transitioning from an abstract description to a concrete implementation has many pitfalls. For example, the basic cryptographic element used with Internet Protocol Security (IPsec), which is known as "encryptthenMAC" is an authenticated encryption scheme with weak security [3]. It is considered secure against a chosenplaintext attack (CPA) [4], and it is also secure against spoofing given that the encryption scheme is CPAsecure and the message authentication code (MAC) cannot be spoofed. However, the concrete instantiation used in IPsec, for example, was found to be insecure. The security of the implementation can also be proven by penetration tests, which reveal weaknesses in the implementation of the security concept that could allow an attacker to penetrate the system.
Example: Secure Email
To illustrate the principle of provably secure software development, consider the example of an encrypted email message (Figure 2). In this case, Alice wants to send an encrypted message to Bob. Bob needs to be able to decrypt the email and verify the signature.
Alice has Bob's public key pkB. For simplicity's sake, I will assume that Alice has verified the key and ensured that it is Bob's. Furthermore, Alice has her own private key skA. Similarly, Bob knows Alice's public key pkA and has his own private key skA. In this case, I will also assume that Bob has verified the authenticity of the key pkA.
The first step is to specify the functionality. In this case we are dealing with authenticated email; consequently, I have two tasks: First, I need to compute an encrypted and authenticated email. This interface is designated Enc+Auth. Second – assuming that the authentication is valid – the encrypted email has to be decrypted. Keeping to the same pattern, I will refer to this interface as Vrfy+Dec.
The second step is to determine the (fairly simple) security properties. The attacker knows Alice and Bob's public keys and all the methods used. Nevertheless, the attacker must not be able to obtain information from the email. Furthermore, the attacker must not be able to send emails on behalf of Alice (i.e., messages verified with the pkA public key) to Bob.
Although these features seem to make sense at an intuitive level, they still leave too much scope for interpretation. Can the attacker interact with Bob? Is there a learning phase where the attacker is allowed to use Alice as an interface to forward the encrypted and authenticated emails from Alice to Bob? Is the attacker allowed to impersonate Bob and read encrypted emails for a period of time? How are the messages to Bob generated? In a formal description of the security properties, it is important to eliminate these ambiguities so that a precise and unambiguous description results.
After formalizing the interfaces and the security properties, the third step is to instantiate the individual components using cryptographic methods. The two interfaces Enc+Auth and Vrfy+Dec need to be constructed with cryptographic procedures such that they provide precisely the desired functions. In the case of secure email, this step is relatively simple (Figure 3).
To implement the Enc+Auth interface, you first need to encrypt the message with a public key method and then sign the ciphertext with a digital signature method. I'll use c to denote the ciphertext and the lowercase Greek letter sigma (s) to denote the signature. In line with this, you would implement the Vrfy+Dec interface with the following operations. First, the signature procedure's verification algorithm is used to check the validity of the signature on the ciphertext c. If this signature is valid, the public key procedure's decryption algorithm decrypts the ciphertext c and outputs the resulting message m.
In the security validation, I can now assume in the fourth step that both the encryption method and the signature method are secure according to formal definitions. You then formally verify that an attack that breaks the security of Enc+Auth as well as Vrfy+Dec (according to the formal model) can be used to break the security of both the public key and the signature procedure. However, since both procedures were assumed to be secure in the first step, a contradiction arises, from which it follows that such an attack cannot exist.
In the last two steps, you now use concrete procedures, for example, RSAbased encryption, implement them, and prove the security of the implementation through penetration tests.
Strengths and Limitations
Since the discovery of this method, provably secure cryptographic methods such as El Gamal encryption [4] have been virtually unbreakable. Provable security reduces the proof for an encryption method to a simple computational problem, such as the very wellknown factorization problem.
In this problem, the attacker is given a number N=p*q calculated as the product of two primes of equal length p and q. The attacker's task is now to compute the two prime factors p and q. To date, no efficient solution algorithm has been discovered for this wellknown computational problem. If the security of an encryption scheme is now based on the factorization problem, then the formal proof shows the following. If there is an efficient attacker who breaks the encryption scheme, then there is also an efficient attacker who solves the factorization problem. In other words, the problem of breaking the encryption is as difficult to solve as the factorization problem.
At first glance, the term "provably secure" suggests that there are provably no longer any attacks. However, this is not true. Attacks on systems that are supposedly probably secure repeatedly occur. Where does this contradiction come from, and how can it be resolved? First of all, it is important to note that the security of the proof always refers to a formal model. However, if the model does not truly reflect practice, then it cannot rule out potential attacks because these attacks simply do not occur in the model. Consequently, accurately modeling reality is one of the biggest challenges in this area, and even the smallest errors in modeling can lead to an insecure solution.
The security of the Secure Sockets Layer (SSL) protocol is a great example of incomplete modeling. In practice it was possible for a message not to be decrypted; instead, a Padding Error message appeared. At first glance, this appears harmless, as it does not seem to reveal any direct information about the plaintext. This is why it was not included in the formal model. At second glance, however, researchers were able to show that it was possible to exploit this error message to decrypt the full message – and to do so without breaking the actual security of the encryption scheme.
« Previous 1 2 3 4 Next »
Buy this article as PDF
(incl. VAT)
Buy Linux Magazine
Subscribe to our Linux Newsletters
Find Linux and Open Source Jobs
Subscribe to our ADMIN Newsletters
Support Our Work
Linux Magazine content is made possible with support from readers like you. Please consider contributing when you've found an article to be beneficial.
News

PipeWire 1.0 Officially Released
PipeWire was created to take the place of the ofttroubled PulseAudio and has finally reached the 1.0 status as a major update with plenty of improvements and the usual bug fixes.

Rocky Linux 9.3 is Available for Download
The latest version of the RHEL alternative is now available and brings back cloud and container images for ppc64le along with plenty of new features and fixes.

Ubuntu Budgie Shifts How to Tackle Wayland
Ubuntu Budgie has yet to make the switch to Wayland but with a change in approaches, they're finally on track to making it happen.

TUXEDO's New Ultraportable Linux Workstation Released
The TUXEDO Pulse 14 blends portability with power, thanks to the AMD Ryzen 7 7840HS CPU.

AlmaLinux Will No Longer Be "Just Another RHEL Clone"
With the release of AlmaLinux 9.3, the distribution will be built entirely from upstream sources.

elementary OS 8 Has a Big Surprise in Store
When elementary OS 8 finally arrives, it will not only be based on Ubuntu 24.04 but it will also default to Wayland for better performance and security.

OpenELA Releases Enterprise Linux Source Code
With Red Hat restricting the source for RHEL, it was only a matter of time before those who depended on that source struck out on their own.

StripedFly Malware Hiding in Plain Sight as a Cryptocurrency Miner
A rather deceptive piece of malware has infected 1 million Windows and Linux hosts since 2017.

Experimental Wayland Support Planned for Linux Mint 21.3
As with most Linux distributions, the migration to Wayland is in full force. While some distributions have already made the move, Linux Mint has been a bit slower to do so.

Window Maker Live 0.96.00 Released
If you're a fan of the Window Maker window manager, there's a new official release of the Linux distribution that champions the oldschool user interface.