TY - GEN
T1 - hacspec
T2 - 4th Conference on Security Standards Research, SSR 2018
AU - Bhargavan, Karthikeyan
AU - Kiefer, Franziskus
AU - Strub, Pierre Yves
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018/1/1
Y1 - 2018/1/1
N2 - We present hacspec, a collaborative effort to design a formal specification language for cryptographic primitives. Specifications (specs) written in hacspec are succinct, easy to read and implement, and lend themselves to formal verification using a variety of existing tools. The syntax of hacspec is similar to the pseudocode used in cryptographic standards but is equipped with a static type system and syntax checking tools that can find errors. Specs written in hacspec are executable and can hence be tested against test vectors taken from standards and specified in a common format. Finally, hacspec is designed to be compilable to other formal specification languages like F*, EasyCrypt, Coq, and cryptol, so that it can be used as the basis for formal proofs of functional correctness and cryptographic security using various verification frameworks. This paper presents the syntax, design, and tool architecture of hacspec. We demonstrate the use of the language to specify popular cryptographic algorithms, and describe preliminary compilers from hacspec to F* and to EasyCrypt. Our goal is to invite authors of cryptographic standards to write their pseudocode in hacspec and to help the formal verification community develop the language and tools that are needed to promote high-assurance cryptographic software backed by mathematical proofs.
AB - We present hacspec, a collaborative effort to design a formal specification language for cryptographic primitives. Specifications (specs) written in hacspec are succinct, easy to read and implement, and lend themselves to formal verification using a variety of existing tools. The syntax of hacspec is similar to the pseudocode used in cryptographic standards but is equipped with a static type system and syntax checking tools that can find errors. Specs written in hacspec are executable and can hence be tested against test vectors taken from standards and specified in a common format. Finally, hacspec is designed to be compilable to other formal specification languages like F*, EasyCrypt, Coq, and cryptol, so that it can be used as the basis for formal proofs of functional correctness and cryptographic security using various verification frameworks. This paper presents the syntax, design, and tool architecture of hacspec. We demonstrate the use of the language to specify popular cryptographic algorithms, and describe preliminary compilers from hacspec to F* and to EasyCrypt. Our goal is to invite authors of cryptographic standards to write their pseudocode in hacspec and to help the formal verification community develop the language and tools that are needed to promote high-assurance cryptographic software backed by mathematical proofs.
U2 - 10.1007/978-3-030-04762-7_1
DO - 10.1007/978-3-030-04762-7_1
M3 - Conference contribution
AN - SCOPUS:85057821999
SN - 9783030047610
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 20
BT - Security Standardisation Research - 4th International Conference, SSR 2018, Proceedings
A2 - Cremers, Cas
A2 - Lehmann, Anja
PB - Springer Verlag
Y2 - 26 November 2018 through 27 November 2018
ER -