This project aims to obtain provably optimal cryptographic constructions, using objectively practical techniques, for a wide range of tasks. To achieve this goal, the project makes progress on three technical fronts. First, a general-purpose framework is developed that encompasses and systematizes known practical cryptographic techniques from many domains. Second, the project develops techniques for proving concrete, fine-grained lower bounds about constructions within this framework. Finally, techniques from program synthesis will be applied to the new framework. These techniques culminate in methods for automatically synthesizing secure and optimal cryptographic constructions. This project focuses on cryptographic constructions that use fast, practical techniques. Such constructions are the most likely to have immediate impact on everyday use. The cryptographic applications areas being studied range from fundamental ones already in widespread use, such as symmetric-key encryption and digital signatures, to more advanced ones more recently approaching practical adoption like garbled circuits. The project also advances undergraduate and graduate education in cryptography with the ongoing development of comprehensive and innovative curricular materials