The security of cryptographic libraries relies on both the security of the underlying cryptographic primitives and their correct implementation. To obtain strong security guarantees, it is desirable to develop formal computer-checked proofs for both since it is difficult to deal with the inherent complexity and to prevent mismatches between algorithmic specifications and implementations otherwise. In this talk, I will focus on computer-aided proofs of key exchange protocols and pairing-based crypto. In particular, I will present a new modular security proof for key exchange protocols in EasyCrypt and a new tool that supports extremely compact, and often fully automated, proofs of cryptographic constructions based on pairing groups. The tool uses a new formal logic which captures key reasoning principles in provable security, and operates at a level of abstraction that closely matches cryptographic practice. To obtain stronger guarantees and allow for proof reuse in different contexts, the tool also generates proofs that are independently verifiable in EasyCrypt.