Homotopy Type Theory and Synthetic Approaches to Mathematical Foundations with Applications to Formal Verification of Cryptographic Protocols

This dissertation develops original contributions within homotopy type theory as a synthetic foundation for mathematics, establishing new results on higher inductive types and their computational semantics, with a novel application domain in the formal verification of cryptographic protocols deployed in Nigerian financial technology and e-government systems. Homotopy type theory, which interprets types as topological spaces and propositions as types, provides a unified logical and geometric foundation for mathematics that is both computable and amenable to mechanised theorem proving, and its application to the formal verification of security protocols addresses the critical gap between abstract protocol specifications and the rigorous mathematical proofs of security properties required for high-assurance financial applications. The dissertation develops constructive proofs of the univalence axiom consequences in the context of parameterised higher inductive types representing cryptographic data structures including Merkle trees, elliptic curve point groups, and zero-knowledge proof systems. Original homotopy-level characterisations of cryptographic indistinguishability relations are formulated within the internal language of the infinity-topos of spaces, and a synthetic definition of computational security reductions is developed that captures the polynomial-time constraint through cohesive type theory modalities. The resulting framework is applied to the formal verification of the Schnorr identification protocol and a simplified version of the BLS aggregate signature scheme deployed in a Nigerian digital identity management system, providing mechanised proofs in the Agda proof assistant. Keywords: homotopy type theory, formal verification, cryptographic protocols, higher inductive types, digital identity