Verifying and Monitoring the Lightweight Directory Access Protocal (LDAP)

Zusammenfassung

The Lightweight Directory Access Protocol (LDAP) plays a crucial role in modern enterprise infrastructure for centralized authentication and authorization, yet lacks comprehensive formal verification. We develop a formal model capturing LDAP and its most popular authentication mechanisms (Simple Bind, SASL PLAIN, SASL-CRAM-MD5, SASL SCRAM-SHA-256 and SASL SCRAM-SHA-256-PLUS). We bridge the gap between this formal model and the most widely used implementation of the protocol, OpenLDAP, by monitoring it using the SpecMon framework. We instrument the cryptographic library to generate an event stream which SpecMon continuously checks for compliance with the model. We use Tamarin to prove authentication properties, which thus transfer to OpenLDAP.