Búsqueda avanzada

Gaining Trust by Tracing Security Protocols

(Artículo ya publicado)


In this article we test an Erlang implementation of the NoiseProtocol 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. Testingtypically performs a noise protocol handshake between thetwo 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: Duringthe handshake the Erlang noise implementation is traced.The resulting protocol trace is refactored, obtaining as theend result a symbolic description (a functional term) of howkey protocol values are constructed using cryptographic op-erations and keys. Therafter, this symbolic term is compared,using term rewriting, with a symbolic term representing theideal symbolic execution of the tested noise protocol hand-shake (i.e., the “semantics” of the handshake). The semanticsymbolic term is obtained by executing a symbolic imple-mentation of the noise protocol that we have developed.

Palabras Clave:

Erlang - Noise - Original publication in the 2019 ACM SIGPLAN Erlang Workshop. - Security Protocols - Tracing





Acceso a los detalles haciendo click aquí.