Home / Papers / Cryptol: high assurance, retargetable crypto development and validation

Cryptol: high assurance, retargetable crypto development and validation

53 Citations2003
Jeffrey R. Lewis, Galois
IEEE Military Communications Conference, 2003. MILCOM 2003.

A new, formal methods-based approach to the specification and implementation of cryptography is introduced, a number of scenarios of use, an overview of the language, and part of a specification of the advanced encryption standard are presented.

Abstract

As cryptography becomes more vital to the infrastructure of computing systems, it becomes increasingly vital to be able to rapidly and correctly produce new implementations of cryptographic algorithms. To address these challenges, we introduce a new, formal methods-based approach to the specification and implementation of cryptography, present a number of scenarios of use, an overview of the language, and present part of a specification of the advanced encryption standard.