Lean, informalized

Nielsen & Chuang · Chapter 12, Quantum information theory · p. 584

Exercise 12.25 - One private key for each pair of users, one public key for each user

Counting the keys a network of users needs.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

A network of nn users wants every pair of them to be able to talk in secret. With private key cryptography, each pair shares a key of its own, known to the two of them and to no one else. Public key cryptography instead lets each user publish a single key, with which anyone can encrypt a message that only that user can read. The exercise counts the keys each scheme needs as the network grows.

Users and Keys

The users form a finite set VV, and nn is the number of its elements.

The set KprivK_{\mathrm{priv}} of private keys of VV holds one key for each unordered pair of distinct users: Kpriv={{u,v}:u,v∈V,u≠v}.K_{\mathrm{priv}} = \bigl\{\, \{u,v\} : u, v \in V,\ u \neq v \,\bigr\}.(1)✦

The set KpubK_{\mathrm{pub}} of public keys of VV holds one key for each user, and is the set of users itself: Kpub=V.K_{\mathrm{pub}} = V.(2)✦

The Claim

Theorem 1. Let VV be a finite set of nn users. The number of private keys of VV is |Kpriv|=n(n−1)2,|K_{\mathrm{priv}}| = \frac{n(n-1)}{2},(3)✦ and the number of public keys of VV is |Kpub|=n.|K_{\mathrm{pub}}| = n.(4)✦

What Is Checked

The claim is stated over the private keys (1) and the public keys (2) of a finite set of users. The library proves both counts, (3) for the pairs and (4) for the users.