Abstract

This paper presents a new approach for the formal specification of cryptographic schemes using types. It discusses specifying a cryptographic protocol using homotopy type theory which adds the notion of higher inductive type and univalence to Martin-L¨of’s intensional type theory. A higher inductive type allows us to introduce constructors for paths and higher-dimensional paths in addition to points. Equivalences or bijections in the universe can identify the paths through univalence. A higher inductive type specification 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 of mappings in homotopy type theory, the path structure will be preserved in the mapping and realized by equivalence in the universe. The higher inductive type gives us a graphical computational model and can be used to extract functions from underlying concrete implementation. Using this model we can achieve various guarantees on the correctness of the cryptographic implementation.