A Type-based Formal Specification for Cryptographic Protocols

Paventhan Vivekanandan+

 

Indiana University, Bloomington, IN, USA

pvivekan@umail.iu.edu

 

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öf’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.

Keywords: Higher Inductive Type, Univalence, Functor, Homotopy, Groupoid, Universe, Equivalence,

Quasi-inverse, Identity type

 

+: Corresponding author: Paventhan Vivekanandan
School of Informatics, Computing and Engineering, Indiana University, Bloomington, Indiana, USA,
Tel: +1-812-369-6576

 

Journal of Internet Services and Information Security (JISIS), 8(4): 16-36, November 2018
DOI: 10.22667/JISIS.2018.11.30.016 [pdf]