ABSTRACT. We present a new direction for the formal specification of cryptographic schemes using types. In this approach, we specify a cryptographic protocol using the tools of homotopy type theory. Homotopy type theory adds the notion of higher inductive type and univalence axiom to Martin-Löf’s intensional type theory. A higher inductive type allows us to introduce constructors for paths and higher-dimensional paths in addition to points. The paths are then identified by equivalences in the universe through univalence. A higher inductive type can act as a front-end mapped to a concrete cryptographic implementation in the universe. By having a higher inductive type front-end, we can encode domain-specific laws of the cryptographic implementation as higher-dimensional paths. Due to univalence and functoriality, the path structure will be preserved in the mapping and realized by equivalence in the universe. Using this model we can achieve various guarantees on the correctness of the cryptographic implementation.