CO 487: Applied Cryptography

Alfred Menezes

Estimated study time: 50 minutes

Table of contents

Based on lecture notes by Sibelius Peng — PDF source

Sources and References

Primary textbook — Boneh, D. and Shoup, V. A Graduate Course in Applied Cryptography. Draft textbook, freely available at crypto.stanford.edu/~dabo/cryptobook/. Supplementary texts — Katz, J. and Lindell, Y. Introduction to Modern Cryptography, 3rd ed. CRC Press, 2020. Menezes, A., Oorschot, P., and Vanstone, S. Handbook of Applied Cryptography. CRC Press, 1996 (freely available at cacr.math.uwaterloo.ca/hac/). Online resources — Dan Boneh’s Cryptography I and II (Coursera/Stanford). MIT 6.875 Cryptography (Goldwasser–Micali lecture notes). Christof Paar’s Introduction to Cryptography lectures (YouTube). Lecture notes — Peng, S. CO 487 Lecture Notes (Winter 2021). https://pdf.sibeliusp.com/1211/co487.pdf

Chapter 1: Security Goals and the TLS Protocol

Cryptography is the study of techniques for securing communication in the presence of adversaries. In modern usage, it encompasses far more than secrecy: authentication, integrity, non-repudiation, and forward secrecy are all cryptographic goals, and real protocols must satisfy all of them simultaneously.

The canonical motivating example is HTTPS — the secure web. When you connect to your bank’s website, your browser and the bank’s server execute the Transport Layer Security (TLS) handshake, which:

  1. Authenticates the server using a digital certificate signed by a trusted certificate authority (CA).
  2. Establishes a shared secret using a key exchange algorithm (typically Elliptic Curve Diffie–Hellman).
  3. Derives session keys for a symmetric cipher (typically AES) and a MAC (typically HMAC-SHA256 or AEAD like AES-GCM).
  4. Encrypts all subsequent data with those session keys.

Every component of this pipeline — digital certificates, elliptic curve key exchange, AES, hash functions, MACs — is a separate cryptographic primitive, and CO 487 studies each one in depth. The security proofs are reductionist: a cryptosystem is secure if breaking it implies breaking a hard mathematical problem (factoring, discrete logarithm, collision finding) — and the course examines both the proofs and the real-world attacks that arise when implementations deviate from the ideal.

Cryptography in Context

A cryptosystem provides guarantees against adversaries with bounded computational resources. Classical cryptography assumed computational secrecy was impossible and focused on information-theoretic security (the one-time pad). Modern cryptography accepts computational assumptions — RSA hardness, discrete logarithm hardness — and derives rich functionality from them.

Kerckhoffs’ principle: a cryptosystem should be secure even if everything about the system except the key is public knowledge. Security through obscurity is not security at all.

Security notions. The most important security property for encryption is semantic security (also called IND-CPA — indistinguishability under chosen-plaintext attack): an adversary who can encrypt messages of their choice cannot distinguish encryptions of two messages of equal length. For authentication, the analogous notion is EUF-CMA (existential unforgeability under chosen-message attack).

Chapter 2: Symmetric-Key Cryptography

Symmetric-key cryptography uses a shared secret key known to both sender and receiver. It provides fast encryption of bulk data and is the workhorse of real-world secure communication — even when a public-key system is used for key establishment, subsequent data is always encrypted with a symmetric cipher.

Classical Ciphers and Their Weaknesses

Simple substitution ciphers replace each plaintext character with a fixed ciphertext character. The English alphabet gives a keyspace of \(26!\) keys — far too large to enumerate — but language statistics break them immediately. Letter frequencies (E is the most common letter in English at ~12.7%, followed by T at ~9.1%) reduce breaking a substitution cipher to a pattern-matching puzzle solvable in minutes.

Polyalphabetic ciphers (Vigenère) use a repeating key to apply multiple substitutions, defeating simple frequency analysis. The Kasiski test and index of coincidence recover the key length, after which each position reduces to a monoalphabetic cipher. Both classical attacks exploit the redundancy of natural language: a true random string has entropy 1 bit per bit, while English text has entropy roughly 1.1 bits per character.

The one-time pad achieves information-theoretic security: XOR the message with a truly random key of equal length. Shannon proved this is the unique scheme achieving perfect secrecy. The catch is key distribution — the key must be as long as the message and never reused — making the OTP impractical for most applications.

Stream Ciphers

A stream cipher uses a short key and a PRNG (pseudorandom number generator) to generate a long keystream, which is then XOR’d with the plaintext. Security reduces to the pseudorandomness of the keystream: if the PRNG is computationally indistinguishable from truly random, the stream cipher achieves semantic security.

RC4 (Rivest Cipher 4, 1987) generates a keystream via a key-scheduling algorithm on a 256-byte state array, followed by a pseudorandom generation algorithm. It was widely used in SSL/TLS and WEP. However, the Fluhrer–Mantin–Shamir attack (2001) on WEP showed that the first bytes of the RC4 keystream are correlated with the key when IVs are chosen sequentially. WEP concatenated the three-byte IV with the key, and collecting 4–10 million packets allows full key recovery in seconds. RC4 is deprecated in all modern protocols.

\[ a \mathrel{+}= b;\; d \mathrel{\oplus}= a;\; d \lll 16;\quad c \mathrel{+}= d;\; b \mathrel{\oplus}= c;\; b \lll 12;\quad \ldots \]

Each round mixes the state via addition, XOR, and rotation — operations that are fast in software. ChaCha20 has no known distinguishing attacks and is used in TLS 1.3 (paired with Poly1305 for authentication as ChaCha20-Poly1305).

Block Ciphers: AES

A block cipher is a keyed permutation \(E_K : \{0,1\}^n \to \{0,1\}^n\). Security requires that \(E_K\) behaves like a pseudorandom permutation (PRP): no efficient adversary can distinguish \(E_K\) from a truly random permutation.

DES (Data Encryption Standard, 1977) uses 56-bit keys and 64-bit blocks. A meet-in-the-middle attack breaks Double-DES: the attacker enumerates \(2^{56}\) first-half encryptions and \(2^{56}\) second-half decryptions and looks for collisions — reducing a brute force from \(2^{112}\) to \(2^{57}\) time with \(2^{56}\) storage. Triple-DES with keying option 1 (three independent keys) achieves an effective 112-bit security level.

AES (Advanced Encryption Standard, 2001; originally Rijndael by Daemen–Rijmen) uses 128-bit blocks and 128/192/256-bit keys. Its round function operates on a \(4 \times 4\) byte state and has four steps:

  1. SubBytes — apply the S-box (invertible nonlinear substitution \(b \mapsto b^{-1}\) in \(\mathbb{F}_{2^8}\)) to each byte.
  2. ShiftRows — cyclically shift row \(i\) left by \(i\) bytes.
  3. MixColumns — multiply each column by a fixed \(4 \times 4\) matrix over \(\mathbb{F}_{2^8}\).
  4. AddRoundKey — XOR the state with the round key derived from the key schedule.

AES-128 runs for 10 rounds. The design principles of confusion (SubBytes, nonlinearity) and diffusion (ShiftRows, MixColumns) come from Shannon’s original analysis of secure ciphers. After 25 years of public cryptanalysis, the best known attack on AES-128 is a related-key attack with complexity \(2^{126.1}\), so AES is essentially unbroken in standard settings.

Modes of Operation

A block cipher encrypts single blocks; modes of operation extend it to arbitrary-length messages:

  • ECB (Electronic Codebook): encrypt each block independently. Deterministic — identical plaintext blocks give identical ciphertext blocks. Catastrophically insecure for images (the “ECB penguin”).
  • CBC (Cipher Block Chaining): \(c_i = E_K(m_i \oplus c_{i-1})\). Secure for IND-CPA with random IV, but malleable (flipping a ciphertext bit predictably flips a plaintext bit in the next block).
  • CTR (Counter): \(c_i = m_i \oplus E_K(IV \| i)\). Turns a block cipher into a stream cipher. Parallelisable, fast, and IND-CPA secure. Does not provide integrity.

Chapter 3: Hash Functions

A cryptographic hash function \(H : \{0,1\}^* \to \{0,1\}^n\) maps arbitrary-length inputs to fixed-length digests. Three security properties are required:

Definition (Security properties of hash functions).

  • Preimage resistance (one-wayness): given \(y\), it is hard to find \(x\) with \(H(x) = y\).
  • Second-preimage resistance: given \(x\), it is hard to find \(x' \neq x\) with \(H(x') = H(x)\).
  • Collision resistance (CR): it is hard to find any pair \(x \neq x'\) with \(H(x) = H(x')\).

These are ordered by strength: CR implies second-preimage resistance (in a slightly weaker sense), but not preimage resistance. Preimage resistance does not imply CR.

Birthday Attacks

Generic collision finding exploits the birthday paradox: if \(H\) has \(n\)-bit output, collecting \(\approx 2^{n/2}\) random images produces a collision with constant probability. This is optimal for black-box hash functions — no better generic attack is known. For preimages, the optimal attack takes \(\approx 2^n\) evaluations.

The Pollard rho / van Oorschot–Wiener parallel collision search finds collisions using only \(O(1)\) memory. The iteration \(x_{i+1} = H(x_i)\) eventually cycles; detecting the cycle (via Floyd’s or Brent’s algorithm) gives a collision. With \(P\) processors, collision finding takes time \(O(2^{n/2}/P)\).

Merkle–Damgård Construction

The dominant paradigm for hash function design is the Merkle–Damgård construction: divide the message into fixed-size blocks, apply a compression function \(f : \{0,1\}^{n} \times \{0,1\}^b \to \{0,1\}^n\) iteratively, and output the final chaining value (after appending length padding).

Theorem (Merkle–Damgård security reduction). If the compression function \(f\) is collision-resistant, then the hash function \(H\) built by Merkle–Damgård is collision-resistant.

SHA-1 (160 bits, deprecated), SHA-256 (256 bits, standard), SHA-512 (512 bits) are all Merkle–Damgård constructions. SHA-256 processes 512-bit blocks using a compression function with 64 rounds of message mixing and nonlinear step functions derived from fractional parts of square roots of primes. Wang et al. (2005) found SHA-1 collisions in \(2^{69}\) operations (improved to \(2^{63.1}\) by Stevens 2013); SHA-1 is now broken for collision resistance. SHA-256 remains secure.

SHA-3 (Keccak, standardised 2012) uses the sponge construction instead of Merkle–Damgård. The sponge absorbs input by XORing into the “rate” portion of the state and applying a permutation; output is squeezed out. SHA-3 is resistant to length-extension attacks that afflict Merkle–Damgård.

Chapter 4: Message Authentication Codes

A message authentication code (MAC) scheme provides integrity: given key \(K\) and message \(m\), the tag \(\text{MAC}_K(m)\) lets the recipient verify that \(m\) was not tampered with and came from someone knowing \(K\). The security notion is EUF-CMA: an adversary who can query \(\text{MAC}_K\) on chosen messages cannot forge a valid \((m^*, t^*)\) pair for any new message \(m^*\).

CBC-MAC and HMAC

CBC-MAC: encrypt the message using CBC mode (with zero IV) and output the final block. This is secure for fixed-length messages: the tag of a length-\(\ell\) message is the last CBC output block, and forgery requires guessing a block cipher output. For variable-length messages, CBC-MAC is insecure: if \(\text{MAC}(m) = t\), then \(\text{MAC}(m \| m' \oplus t) = \text{MAC}(m')\) for any \(m'\), giving a length-extension forgery. EMAC (Encrypted MAC) fixes this by encrypting the final tag with a second independent key.

\[ \text{HMAC}_K(m) = H((K \oplus \text{opad}) \| H((K \oplus \text{ipad}) \| m)), \]

where opad and ipad are fixed padding constants. HMAC is secure as long as \(H\) is a pseudorandom function (PRF), a weaker requirement than collision resistance. HMAC-SHA256 is the standard MAC in TLS 1.2 record protection.

Authenticated Encryption: AES-GCM

Modern protocols use authenticated encryption with associated data (AEAD), which simultaneously provides confidentiality, integrity, and authentication of associated data (like headers) in a single pass. AES-GCM (Galois/Counter Mode) is the dominant AEAD:

  1. Encrypt: use AES-CTR to produce ciphertext \(C\).
  2. Authenticate: compute a GHASH authentication tag over the associated data \(A\), ciphertext \(C\), and their lengths, using a Galois field multiplication with key \(H = E_K(0^{128})\).
\[ \text{GHASH}_H(A, C) = (A_1 \cdot H^{m+n+1} + \cdots + C_n \cdot H^{n+1} + L \cdot H) \cdot H, \]

where \(L\) encodes the lengths. AES-GCM achieves IND-CPA encryption and INT-CTXT authentication. The one critical caveat is nonce reuse: if two messages are encrypted with the same nonce, the GHASH key \(H\) is recoverable from the ciphertext, breaking authentication completely. Real implementations (TLS, SSH) use sequence numbers as nonces to prevent reuse.

Chapter 5: Public-Key Cryptography: Foundations

Symmetric-key cryptography requires a pre-shared secret, which creates a key distribution problem: \(n\) parties who want pairwise secure communication need \(\binom{n}{2}\) shared keys established over a secure channel — which is circular (you need security to establish the keys). Public-key cryptography solves this.

Diffie–Hellman Key Exchange

Whitfield Diffie and Martin Hellman (1976) introduced the revolutionary idea of exchanging keys publicly without prior shared secret, based on a computational hardness assumption.

Protocol. Fix a prime \(p\) and a generator \(g\) of \(\mathbb{Z}_p^*\).

  1. Alice chooses secret \(a \xleftarrow{R} \{1, \ldots, p-2\}\), sends \(A = g^a \bmod p\).
  2. Bob chooses secret \(b \xleftarrow{R} \{1, \ldots, p-2\}\), sends \(B = g^b \bmod p\).
  3. Both compute the shared key \(K = g^{ab} \bmod p = A^b = B^a\).

Security. The Computational Diffie–Hellman (CDH) assumption says: given \(g, g^a, g^b\), it is hard to compute \(g^{ab}\). The Decisional Diffie–Hellman (DDH) assumption says: \((g, g^a, g^b, g^{ab})\) is computationally indistinguishable from \((g, g^a, g^b, g^c)\) for random \(c\). DDH implies CDH implies DLP (discrete logarithm is hard), but the converses are not known.

Merkle puzzles (proposed before Diffie–Hellman by Ralph Merkle, published 1978) give an \(O(n^2)\) advantage for Alice and Bob over an eavesdropper who needs \(O(n^2)\) work — but this was exponentially worse than DH. The DH system gives an exponential separation.

Algorithmic Number Theory Background

RSA and DH security rests on the hardness of integer factoring and discrete logarithm. Key algorithms:

  • Extended Euclidean algorithm: computes \(\gcd(a, b)\) and Bezout coefficients in \(O(\log^2 n)\) bit operations.
  • Fast modular exponentiation (square-and-multiply): \(a^e \bmod n\) in \(O(\log e)\) multiplications.
  • Miller–Rabin primality test: probabilistic; on a random 2048-bit number, a prime is found after \(\approx 1000\) trials.
  • Chinese Remainder Theorem (CRT): \(\mathbb{Z}_{mn} \cong \mathbb{Z}_m \times \mathbb{Z}_n\) when \(\gcd(m, n) = 1\). Computations mod \(n = pq\) can be split and then combined, a key speedup for RSA decryption.

Chapter 6: RSA — Encryption, Signatures, and Attacks

RSA (Rivest–Shamir–Adleman, 1977) is the most deployed public-key cryptosystem. Its security rests on the integer factorisation problem: given \(n = pq\) (a product of two large primes), it is hard to recover \(p\) and \(q\).

Basic RSA

Key generation. Choose distinct large primes \(p, q\). Set \(n = pq\) and \(\phi(n) = (p-1)(q-1)\). Choose \(e\) with \(\gcd(e, \phi(n)) = 1\), compute \(d = e^{-1} \bmod \phi(n)\). Public key: \((n, e)\). Private key: \(d\).

RSA encryption: \(c = m^e \bmod n\). RSA decryption: \(m = c^d \bmod n\).

Correctness follows from Euler’s theorem: \(c^d = m^{ed} = m^{1 + k\phi(n)} = m \cdot (m^{\phi(n)})^k = m \bmod n\) (using \(\gcd(m, n) = 1\)).

Basic RSA is insecure. Textbook RSA is deterministic: encrypting the same message always gives the same ciphertext (fails IND-CPA). It is also malleable: given \(c = m^e\), the adversary can compute \((2^e \cdot c)^d = 2m\). Practical RSA uses OAEP (Optimal Asymmetric Encryption Padding), which randomises the message before exponentiation.

Integer Factorisation Algorithms

Current records: 829-bit (250-digit) RSA number factored in 2020 by NFS. NIST recommends RSA-2048 for long-term security, RSA-3072 for very long-term.

  • Trial division: \(O(\sqrt{n})\) — feasible only for small factors.
  • Pollard’s \(\rho\) algorithm: finds a factor of \(n\) in \(O(n^{1/4})\) time — useful when \(n\) has a small factor.
  • Quadratic sieve (QS): runs in \(L_n[1/2, 1] = e^{(1+o(1))\sqrt{\ln n \ln \ln n}}\) time — sub-exponential.
  • General Number Field Sieve (GNFS): current champion, runs in \(L_n[1/3, 1.923]\) — faster than QS for \(n > 10^{100}\).

The sub-exponential complexity of GNFS is why 2048-bit keys are needed; a fully exponential algorithm would require only 128-bit keys.

RSA Signature Schemes and Bleichenbacher’s Attack

Basic RSA signatures: sign \(m\) as \(\sigma = m^d \bmod n\); verify \(\sigma^e \equiv m \pmod{n}\). Textbook RSA signatures are forgeable: given signatures \(\sigma_1\) on \(m_1\) and \(\sigma_2\) on \(m_2\), the adversary constructs a valid signature \(\sigma_1 \sigma_2 \bmod n\) on \(m_1 m_2\) — an existential forgery. In practice, one signs \(H(m)\) (the hash of the message) and uses a standardised padding scheme.

PKCS#1 v1.5 padding for RSA signatures prepends \(00\;01\;FF\ldots FF\;00\;[ASN.1 OID]\;[H(m)]\). Bleichenbacher’s 2006 attack exploited lenient implementations that accepted signatures where the hash appeared anywhere to the right of the \(00\) byte (rather than at the end). By finding a cube root (for \(e=3\)) of a specially crafted integer, a forgery can be constructed. This attack broke the Firefox, IE, and Opera signature verification implementations and emphasises that correct padding verification is as important as the cryptographic core.

Chapter 7: Elliptic Curve Cryptography

Elliptic curve cryptography (ECC), independently proposed by Neal Koblitz and Victor Miller in 1985, achieves the same security as RSA with much smaller key sizes. A 256-bit ECC key provides roughly the same security as a 3072-bit RSA key, because the best known attack on the elliptic curve discrete logarithm problem (ECDLP) is fully exponential, whereas the best factoring algorithm (GNFS) is sub-exponential.

Elliptic Curves over Finite Fields

\[ E : y^2 = x^3 + ax + b, \quad a, b \in \mathbb{F}_p, \quad 4a^3 + 27b^2 \neq 0, \]

together with a point at infinity \(\mathcal{O}\). The condition \(4a^3 + 27b^2 \neq 0\) ensures the curve is nonsingular (has no cusps or self-intersections).

Point addition on \(E\) makes \(E(\mathbb{F}_p)\) into an abelian group with identity \(\mathcal{O}\). The group law is defined geometrically: to add points \(P\) and \(Q\), draw the line through them, find the third intersection with the curve, and reflect about the \(x\)-axis. In coordinates:

\[ \lambda = \frac{y_2 - y_1}{x_2 - x_1}, \quad x_3 = \lambda^2 - x_1 - x_2, \quad y_3 = \lambda(x_1 - x_3) - y_1. \]\[ \lambda = \frac{3x_1^2 + a}{2y_1}. \]

By Hasse’s theorem, \(|E(\mathbb{F}_p)| = p + 1 - t\) where \(|t| \leq 2\sqrt{p}\). For random curves, \(|E(\mathbb{F}_p)|\) is roughly uniformly distributed in \([p + 1 - 2\sqrt{p},\, p + 1 + 2\sqrt{p}]\).

The ECDLP and Security

Given points \(P\) and \(Q = kP\) on \(E(\mathbb{F}_p)\), the Elliptic Curve Discrete Logarithm Problem (ECDLP) asks for the integer \(k\). The best known algorithm for random elliptic curves is the Pohlig–Hellman + baby-step-giant-step (or Pollard \(\rho\)) attack, running in \(O(\sqrt{n})\) where \(n = |E(\mathbb{F}_p)|\). This is fully exponential in the key size: a 256-bit curve requires \(\approx 2^{128}\) operations.

Contrast with the DLP over \(\mathbb{F}_p^*\): sub-exponential index calculus attacks reduce security below what the group order suggests. For equivalent security, EC keys are 10× shorter than DL keys over multiplicative groups of the same size.

Side-channel attacks are a serious concern for ECC: timing attacks on the double-and-add scalar multiplication algorithm can leak the private key. Montgomery ladder and windowed NAF methods provide constant-time implementations.

ECDH and ECDSA

Elliptic Curve Diffie–Hellman (ECDH) runs DH over \(E(\mathbb{F}_p)\): choose a base point \(G\) of prime order \(n\). Alice picks \(a \xleftarrow{R} \{1, \ldots, n-1\}\), sends \(A = aG\). Bob picks \(b\), sends \(B = bG\). Shared key: \(aB = bA = abG\). Security: CDH over elliptic curves.

TLS 1.3 standardises ECDH with the Curve25519 (Bernstein 2006) and P-256 curves. Curve25519 uses the Montgomery form \(y^2 = x^3 + 486662x^2 + x\) over \(\mathbb{F}_{2^{255}-19}\), chosen for constant-time implementation safety.

ECDSA (Elliptic Curve Digital Signature Algorithm) uses a random nonce \(k\) per signature:

  1. Compute \(R = kG = (r, \cdot)\).
  2. Compute \(s = k^{-1}(H(m) + ar) \bmod n\). Signature: \((r, s)\).
  3. Verification: compute \(u_1 = s^{-1}H(m)$ and $u_2 = s^{-1}r$, check \(u_1 G + u_2 A = R'\) with \(r' = r\).
\[ s_1 - s_2 = k^{-1}(H(m_1) - H(m_2)) \implies k = \frac{H(m_1) - H(m_2)}{s_1 - s_2} \bmod n. \]

This broke the PlayStation 3 (Sony used a fixed nonce \(k\)) and many Bitcoin wallets. The fix is deterministic ECDSA (RFC 6979), which derives \(k = \text{HMAC-DRBG}(d, H(m))\).

Chapter 8: Case Studies — Bluetooth, GSM, and Real-World Failures

The gap between theoretical security proofs and deployed system security is a recurring theme. CO 487 examines real-world protocols to illustrate how cryptographic principles apply — and fail.

WEP and the Fluhrer–Mantin–Shamir Attack

As discussed in Chapter 2, WEP’s mistake was to concatenate a 3-byte IV with the 13-byte WEP key to form the RC4 seed. The FMS attack exploits correlations in RC4’s key scheduling: for IVs of the form \((A+3, N-1, X)\), the third byte of the keystream is biased toward the value \(\text{key}[A+3] + \text{something known}\). By collecting packets with the right IV form, each key byte can be recovered independently with about 60 packets per byte, or 4000 packets total — available in minutes on a busy network.

The lesson: primitives secure in isolation can be catastrophically insecure when composed naively.

Bluetooth Security and the KNOB Attack

Bluetooth uses a negotiated encryption key length of 1 to 16 bytes. The KNOB (Key Negotiation Of Bluetooth) attack (Biham et al., 2019) exploits the absence of authentication in the key-length negotiation phase of the classic Bluetooth pairing protocol. An attacker intercepts the negotiation and forces both parties to use a 1-byte (8-bit) key, then brute-forces the key in real time. This requires being in radio proximity but does not need any prior knowledge. The attack affected all Bluetooth-compliant devices at the time.

The fix requires authenticating the key length negotiation — a lesson about the necessity of binding all security parameters to the session in authenticated channels.

GSM Authentication Weaknesses

GSM (2G) authenticates the subscriber to the network using a challenge-response protocol: the network sends a 128-bit random challenge \(r\), the phone responds with \(\text{SRES} = A3(K_i, r)\) where \(K_i\) is the subscriber key. However, the authentication is unilateral — the phone authenticates to the network but the network does not authenticate to the phone. A false base station (IMSI catcher) can impersonate the network to intercept calls. Furthermore, \(A3\) was often implemented as COMP128, which had algebraic weaknesses allowing key extraction with \(\approx 150{,}000\) queries. This drove the 3GPP to require mutual authentication in 3G (UMTS) and later standards.

Chapter 9: Key Management and TLS

The security of a cryptographic system is only as strong as its key management infrastructure. Public keys must be authenticated — otherwise an active adversary can mount a man-in-the-middle attack by substituting their own public key.

Certification Authorities and PKI

A digital certificate binds a public key to an identity. An X.509 certificate contains the subject’s name, public key, validity period, issuer name, and the CA’s signature over all these fields. The Public Key Infrastructure (PKI) is the hierarchical system of CAs: root CAs (pre-installed in browsers/OSes) certify intermediate CAs, which certify end-entity certificates.

Certificate transparency (CT) is a recent addition: all publicly trusted TLS certificates must be logged in a cryptographically verifiable append-only log (using Merkle trees). Browsers check that certificates appear in a CT log, making it detectable if a CA issues a fraudulent certificate.

TLS 1.3 Handshake

TLS 1.3 (RFC 8446, 2018) is a major simplification over TLS 1.2:

  1. ClientHello: client sends supported cipher suites and key share (ECDH public key for Curve25519 or P-256).
  2. ServerHello: server responds with key share and certificate. Server immediately computes handshake keys and sends encrypted certificate and Finished MAC.
  3. Client Finished: client verifies certificate, computes the same keys, sends Finished.
  4. Application data: encrypted under the session keys, derived by HKDF from the ECDH shared secret.

TLS 1.3 achieves 1-RTT (one round-trip time) for a new connection and 0-RTT (zero-round-trip resumption) using pre-shared keys from a prior session. Forward secrecy is mandatory: ephemeral ECDH keys are discarded after use, so compromise of a long-term key does not expose past sessions.

Chapter 10: Random Bit Generation and Authenticated Protocols

Cryptographic Randomness

Many cryptographic operations require truly random or pseudorandom bits: RSA key generation needs random large primes, ECDSA needs fresh nonces, TLS needs random session keys. Insufficient entropy has been a source of catastrophic failures: Debian’s OpenSSL bug (2008) removed the entropy collection code, generating only \(2^{15}\) possible RSA/DSA keys across all Debian/Ubuntu systems; all were compromised.

Pseudorandom bit generators (PRBGs) expand a short, truly random seed into a long pseudorandom sequence. A PRBG is cryptographically secure if its output is computationally indistinguishable from true randomness. Constructions include CTR-DRBG (AES in counter mode), HMAC-DRBG, and hash-based DRBGs — all standardised by NIST SP 800-90A.

Cloudflare famously seeds their random number generator with video of a lava lamp wall, alongside standard OS entropy — a demonstration that true randomness requires diverse entropy sources.

FIDO U2F and Phishing-Resistant Authentication

FIDO U2F (Universal 2nd Factor) addresses the weakness of passwords by requiring a hardware token. During registration, the token generates an ECDSA key pair tied to the origin; during authentication, the token signs a challenge that includes the origin. This makes phishing impossible: a phishing site has a different origin and cannot get a valid signature from the user’s token.

FIDO2/WebAuthn extends this to password-free authentication, combining a hardware authenticator (biometric or PIN-protected) with a web API.

The Signal Protocol

Signal (Open Whisper Systems, 2013) achieves exceptional security goals: end-to-end encryption, forward secrecy, and break-in recovery (the ability to re-establish security after a key compromise). It is used in Signal, WhatsApp, and Facebook Messenger (in secret chats).

Key ingredient: the Double Ratchet algorithm combines:

  • X3DH (Extended Triple Diffie–Hellman) for initial key agreement using long-term and one-time prekeys.
  • Symmetric ratchet (HKDF chain) for forward secrecy: each message uses a fresh key derived from the previous one.
  • Diffie–Hellman ratchet: each message includes a new ECDH public key, and the shared secret evolves with each DH exchange, providing break-in recovery.

After a key compromise, no past messages (forward secrecy) or future messages after the next DH ratchet step (break-in recovery) can be decrypted.

Chapter 11: Quantum Threats and Post-Quantum Cryptography

Shor’s and Grover’s Algorithms

A sufficiently large quantum computer would break RSA and ECC completely via Shor’s algorithm (1994): it factors integers and solves discrete logarithms in polynomial time \(O(n^3)\), using the quantum Fourier transform to detect periodicity in \(a^x \bmod n\). Current RSA-2048 would fall to a quantum computer with roughly \(4000\) fault-tolerant logical qubits.

Grover’s algorithm provides a quadratic speedup for unstructured search: a function with \(N\) inputs can be inverted in \(O(\sqrt{N})\) quantum operations. For symmetric key cryptography, this halves the effective key length: AES-128 has only 64-bit quantum security, so AES-256 is recommended for long-term post-quantum security.

NIST Post-Quantum Standardization

NIST launched a competition in 2017 to standardize post-quantum algorithms. The final standards (2024):

  • ML-KEM (CRYSTALS-Kyber): Key Encapsulation Mechanism based on Module Learning With Errors (MLWE) lattice problem.
  • ML-DSA (CRYSTALS-Dilithium): Signature based on MLWE.
  • SLH-DSA (SPHINCS+): Hash-based signature, conservative assumption (only requires secure hash functions).

Lattice-based cryptography rests on the hardness of the Learning With Errors (LWE) problem (Regev 2005): given pairs \((a_i, b_i)\) where \(b_i = a_i \cdot s + e_i \bmod q\) with small error \(e_i\), find secret vector \(s\). LWE is NP-hard to solve in the worst case (with a quantum reduction from shortest vector in lattices).

Code-based systems (Classic McEliece, Chapter 8 of CO 331 notes) and hash-based signatures (SPHINCS+) are alternate post-quantum candidates. Hash-based signatures have extremely conservative security: break one requires finding hash collisions.

Chapter 12: Beyond This Course

Natural Next Topics

CO 487 covers applied cryptography with an emphasis on the practical systems deployed today — AES, SHA, RSA, ECC, TLS, Signal, Bitcoin. Several deep theoretical directions extend this foundation, and understanding them requires both the mathematical tools from the course and new ones.

Provable security and simulation-based definitions. The course uses informal notions of security (“breaking the system implies solving a hard problem”), but modern cryptography demands precise, composable security definitions. The simulation paradigm (Goldwasser–Micali, 1984, and Canetti’s Universal Composability, 2001) defines security by requiring that an adversary’s view in the real protocol is computationally indistinguishable from their view in an ideal world where a trusted third party handles everything. This definition is composable: if each component is UC-secure, the composed protocol is too. Without UC security, it is possible to have protocols that are individually secure but insecure when composed — a common source of protocol bugs.

Understanding why IND-CPA and IND-CCA (chosen-ciphertext attack) security are the right definitions for encryption — and how they relate to semantic security, indistinguishability under non-adaptive queries, and security under reuse — requires working through the definitions carefully. The standard textbook treatment is in Katz–Lindell, or in Boneh–Shoup A Graduate Course in Applied Cryptography. Formal verification tools (ProVerif, CryptoVerif, Tamarin) allow protocol security to be checked automatically; mechanised proofs of TLS 1.3 (Bhargavan et al., 2017) and Signal (Cohn-Gordon et al., 2020) have been completed in these tools.

Fully Homomorphic Encryption (FHE). A fully homomorphic encryption scheme allows anyone to evaluate arbitrary functions on encrypted data: given \(\text{Enc}(m)\), compute \(\text{Enc}(f(m))\) without learning \(m\). Gentry’s breakthrough (2009) constructed the first such scheme using ideal lattices and introduced the key technique of bootstrapping: periodically re-encrypting the ciphertext under a fresh key to reduce accumulated noise. Modern FHE schemes divide into families:

  • BFV (Brakerski–Fan–Vercauteren): exact arithmetic on integers modulo a plaintext modulus, suitable for integer and Boolean circuits.
  • CKKS (Cheon–Kim–Kim–Song): approximate arithmetic on real numbers, suitable for machine learning and statistics — CKKS outputs the correct value up to a controlled error.
  • TFHE (Chillotti–Gama–Georgieva–Izabachène): fast gate bootstrapping on binary circuits, enables arbitrary Boolean circuits with per-gate bootstrapping times of ~10ms on CPU (down to ~1ms on GPU).

The performance gap with plaintext has narrowed dramatically: FHE inference on MNIST now takes seconds rather than hours. Applications include privacy-preserving machine learning (computing model inference on encrypted client data), genomic analysis on encrypted health records, and private set intersection at scale. The fundamental open question is whether there is an inherent computational overhead for homomorphic computation (a “lower bound for private computation”) analogous to Shannon’s channel capacity.

Zero-knowledge proofs and succinct arguments. A zero-knowledge proof (ZKP) allows a prover to demonstrate knowledge of a witness \(w\) satisfying a relation \(R(x, w) = 1\) without revealing \(w\). The classical Goldwasser–Micali–Rackoff (1985) definition requires three properties: completeness (a honest prover convinces the verifier), soundness (a cheating prover cannot convince the verifier of a false statement), and zero-knowledge (the verifier learns nothing beyond the truth of the statement).

Modern ZK systems have become practical through the development of zk-SNARKs (Succinct Non-interactive Arguments of Knowledge). Groth16 (2016) produces constant-size proofs (192 bytes) with near-constant verification time, but requires a trusted setup. PLONK (Gabizon–Williamson–Ciobotaru 2019) is a universal SNARK with a single trusted setup for all circuits up to a given size. STARKs (Ben-Sasson et al. 2018) achieve transparency (no trusted setup) and post-quantum security via hash functions, at the cost of larger proof sizes (tens of kilobytes). ZKPs power Zcash’s shielded transactions (prover proves ownership of a coin without revealing the coin), Ethereum L2 rollups (batch transaction proofs), and privacy-preserving identity systems.

Multi-party computation and secret sharing. In MPC, \(n\) parties hold private inputs \(x_1, \ldots, x_n\) and wish to jointly compute \(f(x_1, \ldots, x_n)\) without any party learning another’s input (beyond what the output reveals). Yao’s garbled circuits (1986) achieve two-party MPC with computational security; the BGW protocol (Ben-Or–Goldwasser–Wigderson 1988) achieves information-theoretic MPC for \(n\) parties as long as fewer than \(n/3\) are corrupt. The Shamir secret sharing scheme — splitting a secret \(s\) into \(n\) shares of a random degree-\((t-1)\) polynomial \(p\) with \(p(0) = s\) — is the underlying primitive. Modern protocols (GMW, SPDZ, MOTION, MP-SPDZ) are fast enough for practical private set intersection (comparing medical databases), federated learning (training ML models without sharing data), and secure auction clearing.

Side-channel and physical attacks. CO 487 discusses protocol-level attacks (Bleichenbacher, KNOB, FMS). Physical attacks target the hardware implementing cryptographic algorithms. Differential power analysis (DPA) (Kocher–Jaffe–Jun 1999) statistically correlates the power consumption of a device with predictions based on guessed key bytes. With a few thousand power traces, the full AES key can be extracted from an unprotected implementation. Simple power analysis (SPA) reads the key directly from the power trace of an RSA or ECC scalar multiplication — if the algorithm takes different execution paths for ‘0’ and ‘1’ bits, the key leaks. Countermeasures include masking (randomising intermediate values so their power consumption is independent of the key), blinding (randomising the scalar in ECC), and shuffling (randomising the order of operations). Fault injection attacks deliberately introduce errors (via voltage glitches, clock glitches, or laser pulses) to extract secrets. For example, inducing a single fault in an RSA-CRT implementation reveals the private key via Bellcore’s attack. Hardware security modules (HSMs) and secure enclaves (ARM TrustZone, Intel SGX) attempt to mitigate physical attacks, but SGX itself has been attacked via side channels (Spectre-variant attacks exploiting the shared cache).

Follow-up Courses and Reading

The material in CO 487 is a practitioner’s foundation. Graduate study in cryptography requires both deeper theory (provable security, lattice mathematics) and broader coverage (advanced protocols, system security).

At UWaterloo, the direct continuations are CO 685 (Mathematics of Public-Key Cryptography), which covers the algebraic number theory underlying RSA and elliptic curves at a graduate level — discriminants, complex multiplication, isogenies, and their impact on ECC security. CO 781 Advanced Topics in Cryptography and CS 758 Cryptography cover provable security, interactive proofs, and zero-knowledge proofs rigorously. CO 331 (Coding Theory, same instructor) provides the finite field foundations for BCH/RS codes and code-based cryptography — the McEliece construction uses all of that theory.

Graduate courses at peer universities. Dan Boneh’s CS 355 Topics in Cryptography (Stanford; all lectures on YouTube, lecture notes at crypto.stanford.edu) covers provable security, ZK proofs, MPC, and advanced protocols to a high standard. MIT 6.875 Foundations of Cryptography (Goldwasser–Micali) develops the complete theoretical framework: computational indistinguishability, pseudorandom generators, one-way functions, commitment schemes, and zero-knowledge. CMU 15-356 Introduction to Cryptography and 15-756 Advanced Cryptography cover post-quantum cryptography in depth with a focus on lattice-based schemes. Christof Paar’s Introduction to Cryptography lecture series (YouTube, 24 lectures) is an excellent, accessible companion to CO 487 from a slightly different angle.

Key texts. Boneh and Shoup A Graduate Course in Applied Cryptography (freely available draft at crypto.stanford.edu/~dabo/cryptobook/) is the most current and comprehensive graduate-level reference, covering symmetric and public-key cryptography, protocols, and advanced topics through 2023. Katz and Lindell Introduction to Modern Cryptography, 3rd ed. (CRC Press, 2020) is rigorous and accessible. The Handbook of Applied Cryptography (Menezes–Oorschot–Vanstone; freely available at cacr.math.uwaterloo.ca/hac/) remains the practical reference. Bernstein and Lange Post-Quantum Cryptography (Springer, 2009) covers code-based, lattice-based, hash-based, and multivariate cryptosystems. For ECC: Silverman The Arithmetic of Elliptic Curves, 2nd ed. (Springer, 2009) covers the algebraic geometry; Washington Elliptic Curves: Number Theory and Cryptography, 2nd ed. (CRC, 2008) balances theory and cryptographic application. For side channels: Mangard, Oswald, Popp Power Analysis Attacks: Revealing the Secrets of Smartcards (Springer, 2007) is the standard reference.

Research communities and venues. Cryptography research appears primarily at the IACR (International Association for Cryptologic Research) conferences: CRYPTO (US), EUROCRYPT (Europe), ASIACRYPT (Asia), and the Theory of Cryptography Conference (TCC). IACR’s ePrint archive (eprint.iacr.org) provides free preprints of essentially all cryptography research. The IEEE Security & Privacy (“Oakland”), ACM CCS, and USENIX Security conferences cover applied and systems security.

Open Problems and Active Research

Cryptography in 2025 is in rapid flux, driven by the post-quantum transition, the blockchain revolution, and the deployment of cryptographic techniques in new contexts (ML, cloud computing, distributed systems). The following problems are among the most important and actively researched.

Security of NIST post-quantum standards. The NIST-standardised ML-KEM (Kyber), ML-DSA (Dilithium), and SLH-DSA (SPHINCS+) were designed with substantial security margins. However, the security analysis of lattice-based schemes against quantum algorithms remains incomplete. The best quantum algorithms for the Learning With Errors (LWE) problem are quantum variants of lattice sieving (Laarhoven 2015, Kirshanova et al. 2019), but their concrete performance (in terms of actual gate counts on a fault-tolerant quantum computer) is not fully understood. Tighter quantum security estimates for Kyber/Dilithium — and verification that the selected parameters actually achieve 128 quantum bits of security — are active research goals.

Isogeny-based cryptography and SIDH collapse. SIDH (Supersingular Isogeny Diffie-Hellman) was a promising post-quantum KEM based on the hardness of finding isogenies between elliptic curves. In 2022, Castryck–Decru and Maino–Martindale independently published polynomial-time classical attacks on SIDH, exploiting the additional information leaked by the torsion point images required for efficient arithmetic. SIDH was broken completely and removed from the NIST competition. The deeper question — whether any isogeny-based scheme can be built that is secure and efficient — remains open. CSIDH (using commutative isogeny graphs) and SQIsign (signature scheme) survive but are less efficient.

FHE bootstrapping efficiency. The fundamental bottleneck in FHE is bootstrapping — reducing ciphertext noise by homomorphically evaluating the decryption circuit. Bootstrapping is the most expensive FHE operation, limiting throughput to thousands of operations per second even on modern hardware. Theoretical lower bounds for bootstrapping (does it require superlinear time?) are unknown. Practical improvements using GPUs, custom ASICs (the Intel HESEA project), and algorithmic improvements (blind rotation, FHEW improvements) are active areas of research and engineering.

The one-way function existence question. The entire edifice of symmetric cryptography (PRGs, PRFs, MACs, stream ciphers) rests on the assumption that one-way functions (OWFs) exist — functions easy to compute but hard to invert. But no unconditional proof that OWFs exist is known; their existence would imply P ≠ NP (since an OWF’s inverse cannot be computed in polynomial time, which would collapse the hierarchy). Thus, all of provable cryptography rests on an unproven assumption. Whether the cryptographic hardness assumptions (OWF existence, LWE hardness, discrete log hardness) can be reduced to pure combinatorial complexity statements (like P ≠ NP) is a major open problem at the interface of cryptography and complexity theory.

Privacy-preserving machine learning. Deploying ML on sensitive data (medical records, financial data) requires protecting privacy. FHE, MPC, and differential privacy are three complementary approaches. In federated learning, clients train locally on their data and share gradients — but gradient sharing can leak private data (gradient inversion attacks). Differential privacy (DP) adds calibrated noise to protect against membership inference. The combination of DP with MPC guarantees (DP-MPC) can achieve both computational and statistical privacy simultaneously, but the performance overhead remains high. Practical private ML at scale is an open systems and theoretical challenge.

Cryptographic applications of AI. Large language models can generate plausible-looking cryptographic code but introduce subtle vulnerabilities (incorrect nonce handling, off-by-one errors in CBC-MAC, weak entropy sources). Formal verification of AI-generated cryptographic code, automatic cryptographic protocol analysis using model checking, and AI-assisted cryptanalysis (using LLMs to suggest attack strategies on novel schemes) are emerging areas. The interaction between AI and cryptography — in both directions — is among the newest active research directions.

Quantum key distribution and large-scale deployment. Quantum key distribution (QKD) provides information-theoretic key agreement using quantum channels. BB84 (Bennett–Brassard 1984) is the foundational protocol; practical QKD systems operate over fiber (Toshiba, ID Quantique, China’s Micius satellite). The main obstacle to large-scale deployment is distance limitation: quantum states cannot be amplified without collapsing, limiting direct QKD to ~500 km. Quantum repeaters — devices that extend range via quantum teleportation and entanglement swapping — are under active development but not yet practical. The question of whether a global quantum network can be built before quantum computers break classical PKI is critical for long-term security planning.

Attribute-based encryption and advanced cryptographic constructs. Beyond the standard public-key encryption (one sender, one receiver) and threshold schemes covered in CO 487, attribute-based encryption (ABE) allows ciphertexts to encode a policy over attributes, and decryption succeeds iff the recipient’s key encodes attributes satisfying the policy. For example, a ciphertext might be encrypted under the policy “(department = Finance AND clearance-level ≥ 3) OR (role = auditor)”, and only users whose credentials satisfy this Boolean formula can decrypt. Key-policy ABE (KP-ABE, Goyal–Pandey–Sahai–Waters 2006) embeds the policy in the key; Ciphertext-policy ABE (CP-ABE, Bethencourt–Sahai–Waters 2007) embeds it in the ciphertext. Both constructions use bilinear pairings on elliptic curves — a structure not available in post-quantum settings. Building efficient and expressive ABE that is post-quantum secure (using lattices) is an active research problem; lattice ABE constructions exist but are far less efficient than pairing-based ones.

Functional encryption generalises ABE further: given a ciphertext of \(x\) and a functional key for function \(f\), compute \(f(x)\) — but learn nothing beyond \(f(x)\). This is a powerful generalisation: ABE is functional encryption for the Boolean function “does attribute set satisfy policy”; inner product encryption (for linear functions) is an intermediate step. General-purpose functional encryption would imply obfuscation (computing with encrypted programs), which is known to be achievable under strong cryptographic assumptions (iO, indistinguishability obfuscation) but whose practical security and efficiency remain challenging.

Obfuscation and program protection. Indistinguishability obfuscation (iO) takes a program (circuit) \(C\) and produces a new program \(\mathcal{O}(C)\) that computes the same function, but given two circuits \(C_1, C_2\) computing the same function, \(\mathcal{O}(C_1)\) and \(\mathcal{O}(C_2)\) are computationally indistinguishable. Jain–Lin–Sahai (2021) constructed the first iO from polynomial-hardness assumptions (including LWE), resolving a decade-long open question. iO implies almost all known cryptographic primitives (OWFs, public-key encryption, functional encryption, non-interactive MPC) but the constructions are currently far too inefficient for practice. Diffuse obfuscation — protecting specific algorithms (AES key schedule, software licensing) from white-box reverse engineering — has a large commercial market and remains practically important; provably secure white-box AES constructions do not yet exist despite many commercial products claiming obfuscation.

The cryptography of blockchain and consensus. Bitcoin’s proof-of-work (Nakamoto 2008) and Ethereum’s proof-of-stake (Gasper, 2020) are distributed consensus protocols built on cryptographic primitives. The underlying cryptographic tools — hash chains, Merkle trees, digital signatures (ECDSA for Bitcoin, BLS for Ethereum), and commitment schemes — are drawn directly from CO 487’s material. The open cryptographic question in blockchain is scalability without security degradation: current proof-of-work consensus has 7 transactions per second vs. Visa’s 24,000; zero-knowledge proof systems (STARKs in zkRollups) allow Layer 2 systems to batch thousands of transactions into a single proof verified on-chain. The formal security models for permissionless blockchains (protocols where any node can join) are more complex than traditional distributed systems models, and the security guarantees depend on the fraction of honest hash power (PoW) or stake (PoS) in ways that are still being formalised. Threshold signatures (where \(t\) out of \(n\) key holders must cooperate to sign, without any single party knowing the full key) are essential for multi-party custody of cryptocurrency assets; threshold ECDSA and BLS aggregate signatures are active development areas.

Memory-hard functions and password hashing. CO 487 covers hash functions primarily in the context of integrity (SHA-256, SHA-3) and MACs. A related application is password hashing — where the goal is to make offline dictionary attacks expensive by requiring significant memory or time even for the verifier. bcrypt (Provos–Mazières 1999) uses the Blowfish cipher in an expensive key schedule; scrypt (Percival 2009) was the first memory-hard function, designed so that computing the hash requires \(\Theta(N)\) memory and \(\Theta(N)\) time simultaneously — making brute-force attacks expensive even on ASICs with many parallel cores. The Argon2 family (2015 winner of the Password Hashing Competition, now RFC 9106) extends this with configurable memory, time, and parallelism parameters. The formal notion of memory-hardness is more subtle than it appears: sequential memory-hardness means the function requires large memory when run by a sequential algorithm; parallel memory-hardness means it requires large memory even for highly parallel adversaries. Proving that a function is memory-hard in the parallel sense requires cryptographic graph pebbling arguments (Alwen–Serbinenko 2015). The design and analysis of memory-hard functions — and their applications to password storage, key derivation (Argon2 as a KDF), and ASIC-resistant proof-of-work — is an active research area bridging cryptography, algorithm design, and hardware engineering.

Isogenies and elliptic curve cryptography: post-SIDH landscape. CO 487 covers ECDH and ECDSA, which operate in the group \(E(\mathbb{F}_p)\). Isogeny-based cryptography uses homomorphisms between elliptic curves (isogenies) as a harder problem. After the 2022 SIDH break (polynomial-time classical attack by Castryck–Decru using auxiliary torsion point information), the post-quantum isogeny landscape shifted dramatically. Surviving schemes include: CSIDH (Castryck–Lange–Martindale–Panny–Renes 2018), which operates on the class group action on supersingular curves over \(\mathbb{F}_p\) and avoids auxiliary points; SQIsign (De Feo–Kohel–Leroux–Petit–Wesolowski 2020), a signature scheme whose security rests on the hardness of computing an isogeny of prescribed degree between two given supersingular curves. SQIsign has the most compact post-quantum signatures (177 bytes for NIST level 1) but is very slow to sign (several seconds). The interplay between the algebraic structure of isogeny graphs (Ramanujan graphs — see Lubotzky–Phillips–Sarnak 1988), the hardness of path-finding in these graphs, and the security of cryptographic protocols built on them is a rich research area connecting algebraic number theory, graph theory, and cryptography.

Formal verification of cryptographic protocols. CO 487’s treatment of real-world failures — Heartbleed, BEAST, Bleichenbacher — illustrates that implementation errors are as dangerous as mathematical weaknesses. Formal verification provides machine-checked proofs that implementations are correct. The Cryptol language (Galois Inc.) is a domain-specific language for specifying cryptographic algorithms; SAW (Software Analysis Workbench) verifies that C or LLVM implementations match their Cryptol specifications using SAT solving and symbolic execution. EasyCrypt is a proof assistant for game-based cryptographic proofs, used to verify schemes like OAEP and the HMAC construction. AWS has used the s2n TLS library verified with the CBMC model checker. The ongoing challenge is scaling formal verification to full protocol stacks (TLS 1.3, Signal, Noise Protocol Framework) and to hardware implementations — where timing side channels and fault injection must be part of the security model. Project Everest (Microsoft Research) aims at a verified implementation of the entire TLS 1.3 stack, from specification down to assembly, demonstrating that the gap between a correct proof and a correct running system can be closed.

Back to top