On Proving the Security of Message Authentication Codes Using Lambda-BLL and Hoare Logic

Reduction-based proofs are the standard technique for establishing the security of cryptographic constructions in the computational model. However, encoding such proofs within formal systems remains a difficult task, as these proofs involve probabilistic computation, adversarial interaction, and explicit reasoning about resource bounds and computational efficiency. This thesis studies the use of programming-language techniques for formalizing cryptographic proofs in the computational model. We work within lambda-BLL, a probabilistic lambda calculus whose graded type system characterizes probabilistic polynomial-time computation. To support reasoning about program correctness and cryptographic experiments, we introduce an assertion-annotated extension of lambda-BLL inspired by Hoare logic, together with a lifting procedure that embeds standard typing judgments into the enriched system. Within this framework, we formalize the security of Message Authentication Codes (MACs) constructed from pseudorandom functions by proving existential unforgeability under chosen-message attacks (EUF-CMA). Overall, this work shows that the lambda-BLL calculus is expressive enough to represent classical cryptographic reductions while statically enforcing polynomial-time resource bounds. By extending the calculus with Hoare-style assertions, we enable reasoning about invariants during program execution as well as about stateful references that arise in cryptographic constructions. This demonstrates the potential of the framework as a foundation for the formal verification of proofs in computational cryptography.