|
A Type-based Formal Specification for
Cryptographic Protocols 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 Journal
of Internet Services and Information Security (JISIS), 8(4):
16-36, November 2018 |