Gaining Trust by Tracing Security Protocols





Publicado en

Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021)

Licencia Creative Commons


In this article we test an Erlang implementation of the Noise Protocol Framework, using a novel form of white-box testing. We extend interoperability testing of an Erlang enoise imple- mentation against an implementation of Noise in C. Testing typically performs a noise protocol handshake between the two implementations. If successful, then both implementa- tions are somehow compatible. But this does, for example, not detect whether we reuse keys that have to be newly gen- erated. Therefore we extend such operability testing: During the handshake the Erlang noise implementation is traced. The resulting protocol trace is refactored, obtaining as the end result a symbolic description (a functional term) of how key protocol values are constructed using cryptographic op- erations and keys. Therafter, this symbolic term is compared, using term rewriting, with a symbolic term representing the ideal symbolic execution of the tested noise protocol hand- shake (i.e., the “semantics” of the handshake). The semantic symbolic term is obtained by executing a symbolic imple- mentation of the noise protocol that we have developed.


Acerca de Fredlund, Lars-Ake

Palabras clave

Erlang, Noise, Original Publication In The 2019 ACM SIGPLAN Erlang Workshop, Security Protocols, Tracing
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX