Security protocols and APIs are difficult to specify and implement. A reference or prototype implementation written in C is often the most formal specification at hand. In this paper, we show how general-purpose C verifiers can be used to prove computational security properties, including—for the first time—computational indistinguishability, of protocols and APIs written in C. To do so, we rely on the VCC verifier to prove that the C program has the same observable input-output behaviour as a functional reference implementation written in F#. We then use the F7 type-checker to prove perfect security properties of the reference code assuming ideal cryptographic primitives. Finally, we reduce the security of a probabilistic polynomial-time program that uses concrete cryptographic primitives to the security of the same program using ideal cryptography. We illustrate our method on the implementation of an exemplary key management API, inspired by the next version of the TPM standard.