133 Cryptography — RSA
133.1 Overview
This file develops a small cost-tracking monad TimeM T α, whose values carry both a return value of type \(\alpha \) and an accumulated time cost of type \(T\) (typically \(T = \mathbb {N}\) counting comparisons), together with worked examples (median of three, insertion sort) that prove functional correctness on the returned value and complexity bounds on the recorded cost. It then formalizes the RSA cryptosystem: for distinct primes \(p,q\) and exponents \(e,d\) with \(ed = 1 + k(p-1)(q-1)\), decryption inverts encryption modulo \(n = pq\).
133.2 Declarations
Lifts a value \(a : \alpha \) into the computation \(\langle a, 0\rangle \) of type TimeM T α, i.e. the computation that returns \(a\) at zero time cost.
Given \(m : \texttt{TimeM T α}\) and \(f : \alpha \to \texttt{TimeM T β}\), the bind of \(m\) and \(f\) runs \(f\) on the value returned by \(m\) and returns \(\langle (f\, m.\mathrm{ret}).\mathrm{ret},\; m.\mathrm{time} + (f\, m.\mathrm{ret}).\mathrm{time}\rangle \): the two time costs are added.
The value returned by \(\mathrm{pure}\, a\) is \(a\).
The value returned by the bind of \(m\) with \(f\) is the value returned by \(f\, m.\mathrm{ret}\).
For \(f : \alpha \to \beta \) and \(x : \texttt{TimeM T α}\), the value returned by the mapped computation is \(f(x.\mathrm{ret})\).
The right-sequencing of \(x\) and \(y\) returns the value returned by \(y\, ()\).
The left-sequencing of \(x\) and \(y\) returns \(x.\mathrm{ret}\).
For \(f : \texttt{TimeM T (α → β)}\) and \(x : \texttt{Unit → TimeM T α}\), the application \(\mathrm{seq}\, f\, x\) returns \(f.\mathrm{ret}\bigl((x\, ()).\mathrm{ret}\bigr)\).
The time cost of the bind of \(m\) with \(f\) is \(m.\mathrm{time} + (f\, m.\mathrm{ret}).\mathrm{time}\).
The time cost of \(\mathrm{pure}\, a\) is \(0\).
Mapping a function over a computation does not change its time cost: it is \(x.\mathrm{time}\).
The time cost of the right-sequencing of \(x\) and \(y\) is \(x.\mathrm{time} + (y\, ()).\mathrm{time}\).
The time cost of the left-sequencing of \(x\) and \(y\) is \(x.\mathrm{time} + (y\, ()).\mathrm{time}\).
The time cost of \(\mathrm{seq}\, f\, x\) is \(f.\mathrm{time} + (x\, ()).\mathrm{time}\).
The computation \(\mathrm{tick}\, c\) returns the trivial value and records time cost \(c\); it is the basic way of charging \(c\) units of time.
The value returned by \(\mathrm{tick}\, c\) is the unit value.
The time cost of \(\mathrm{tick}\, c\) is \(c\).
The timed computation returning the larger of two natural numbers \(x,y\), charging one unit of time for the single comparison \(x \le y\).
For \(a,b,c\) in a linear order, the timed computation returning a median of \(a,b,c\) by a nested sequence of comparisons, charging one unit of time per comparison performed.
The value returned by \(\mathrm{median3}\, a\, b\, c\) is a median of \(a\), \(b\), \(c\), in the sense that it lies between at least one of the pairs drawn from \(\{ a,b,c\} \).
The computation \(\mathrm{median3}\, a\, b\, c\) records a time cost of at most \(3\), i.e. it performs at most three comparisons.
Inserts \(x\) into a list, walking the list until the first element \(y\) with \(x \le y\) and charging one unit of time per comparison. On a sorted input it produces the sorted list containing \(x\).
Insertion sort in the time monad: recursively sort the tail and then insert the head using the timed insertion, accumulating the comparisons performed by every insertion step.
The predicate on lists defined recursively: the empty list and singletons are sorted, and \(x :: y :: \mathit{rest}\) is sorted when \(x \le y\) and \(y :: \mathit{rest}\) is sorted.
For any list \(\mathit{xs}\), the predicate IsSorted holds of \(\mathit{xs}\) if and only if \(\mathit{xs}\) is a chain for \(\le \).
For any list \(\mathit{xs}\), the predicate IsSorted holds of \(\mathit{xs}\) if and only if \(\mathit{xs}\) is sorted in the usual pairwise sense with respect to \(\le \).
The value returned by the timed insertion of \(x\) into \(\mathit{xs}\) is the ordinary ordered insertion of \(x\) into \(\mathit{xs}\) for the relation \(\le \).
The value returned by the timed insertion sort of \(\mathit{xs}\) is the ordinary insertion sort of \(\mathit{xs}\) for the relation \(\le \).
The list returned by inserting \(x\) into \(\mathit{xs}\) has length \(\left\lvert \mathit{xs}\right\rvert + 1\).
The list returned by the timed insertion sort of \(\mathit{xs}\) has the same length as \(\mathit{xs}\).
The list returned by inserting \(x\) into \(\mathit{xs}\) is a permutation of \(x :: \mathit{xs}\).
If \(\mathit{xs}\) is sorted, then the list returned by inserting \(x\) into \(\mathit{xs}\) is sorted.
The list returned by the timed insertion sort of \(\mathit{xs}\) is a permutation of \(\mathit{xs}\).
For every list \(\mathit{xs}\), the list returned by the timed insertion sort is sorted.
For every list \(\mathit{xs}\), the output of the timed insertion sort is both sorted and a permutation of \(\mathit{xs}\).
The worst-case comparison recurrence \(T(0) = 0\) and \(T(n+1) = T(n) + n\).
Inserting \(x\) into a list \(\mathit{xs}\) costs at most \(\left\lvert \mathit{xs}\right\rvert \) comparisons.
The time cost recorded by the timed insertion sort of \(\mathit{xs}\) is at most \(T(\left\lvert \mathit{xs}\right\rvert )\), where \(T\) is the insertion sort recurrence.
For every \(n\), the recurrence satisfies \(T(n) \le n^2\).
The time cost recorded by the timed insertion sort of a list \(\mathit{xs}\) of length \(n\) is at most \(n^2\).
Let \(p\) be prime. For every \(c \in \mathbb {N}\) and every \(x \in \mathbb {Z}/p\mathbb {Z}\),
This is the form of Fermat’s little theorem needed for RSA, valid also at \(x = 0\).
Let \(p\) be prime and \(m, ed, c \in \mathbb {N}\) with \(ed = 1 + c(p-1)\). Then \(m^{ed} \equiv m\) in \(\mathbb {Z}/p\mathbb {Z}\), where both sides are the images of natural numbers.
If \(p\) is prime and \(ed = 1 + k(p-1)(q-1)\), then \(m^{ed} \equiv m\) in \(\mathbb {Z}/p\mathbb {Z}\) for every \(m \in \mathbb {N}\).
If \(q\) is prime and \(ed = 1 + k(p-1)(q-1)\), then \(m^{ed} \equiv m\) in \(\mathbb {Z}/q\mathbb {Z}\) for every \(m \in \mathbb {N}\).
Let \(p\) and \(q\) be coprime and suppose \(m^{ed} \equiv m\) both in \(\mathbb {Z}/p\mathbb {Z}\) and in \(\mathbb {Z}/q\mathbb {Z}\). Then \(m^{ed} \equiv m\) in \(\mathbb {Z}/pq\mathbb {Z}\).
The same statement written with the power taken inside the quotient ring: if \(p\) and \(q\) are coprime and \(\bar m^{\, ed} = \bar m\) in \(\mathbb {Z}/p\mathbb {Z}\) and in \(\mathbb {Z}/q\mathbb {Z}\), then \(\bar m^{\, ed} = \bar m\) in \(\mathbb {Z}/pq\mathbb {Z}\).
A public key consists of a modulus \(n \in \mathbb {N}\) and a public exponent \(e \in \mathbb {N}\).
A secret key consists of a public key together with naturals \(p, q, d, k\) and proofs that \(p\) and \(q\) are prime, that \(p \ne q\), that the public modulus satisfies \(n = pq\), and that the exponents satisfy \(e d = 1 + k(p-1)(q-1)\).
Encryption of a message \(m \in \mathbb {N}\) under a public key is \(\bar m^{\, e} \in \mathbb {Z}/n\mathbb {Z}\), using only the public data.
Decryption of a ciphertext \(c \in \mathbb {Z}/n\mathbb {Z}\) under a secret key is \(c^{\, d}\), where \(d\) is the private exponent.
For any secret key and any message \(m \in \mathbb {N}\), decrypting the encryption of \(m\) recovers \(m\):