Learning Assumptions for Verifying Cryptographic Protocols Compositionally

Automated analysis tools for cryptographic protocols can verify sophisticated designs, but lack compositionality. To address this limitation, we investigate the use of automata learning for verifying authentication protocols in an automatic and compositional way. We present Taglierino, a tool for synthesizing specifications for protocol components and checking them in isolation. The specifications can aid the design of protocol variants and speed up verification. Taglierino includes a domain-specific language for protocols, which are compiled to automata and analyzed with the LTSA model checker extended with automata learning. We demonstrate the tool on a series of case studies, including the Needham-Schroeder, Woo-Lam, and Kerberos protocols.