An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation. - Alfredo Pironti 001; Riccardo Sisto (ISCC, 2007)

Soundness Conditions for Message Encoding Abstractions in Formal Security Protocol Models. - Alfredo Pironti 001; Riccardo Sisto (ARES, 2008)

Soundness Conditions for Cryptographic Algorithms and Parameters Abstractions in Formal Security Protocol Models. - Alfredo Pironti 001; Riccardo Sisto (DepCoS-RELCOMEX, 2008)

Formally Sound Refinement of Spi Calculus Protocol Specifications into Java Code. - Alfredo Pironti 001; Riccardo Sisto (HASE, 2008)

Formally-Based Black-Box Monitoring of Security Protocols. - Alfredo Pironti 001; Jan Jürjens (ESSoS, 2010)

Provably correct Java implementations of Spi Calculus security protocols specifications. - Alfredo Pironti 001; Riccardo Sisto (Comput. Secur., 2010)

Sound automatic implementation generation and monitoring of security protocol implementations from verified formal specifications. - Alfredo Pironti 001 (2010)

The Java SPI Framework for Security Protocol Implementation. - Matteo Avalle; Alfredo Pironti 001; Riccardo Sisto; Davide Pozza (ARES, 2011)

JavaSPI: A Framework for Security Protocol Implementation. - Matteo Avalle; Alfredo Pironti 001; Davide Pozza; Riccardo Sisto (Int. J. Secur. Softw. Eng., 2011)

Formal Vulnerability Analysis of a Security System for Remote Fieldbus Access. - Manuel Cheminod; Alfredo Pironti 001; Riccardo Sisto (IEEE Trans. Ind. Informatics, 2011)

Visual Model-Driven Design, Verification and Implementation of Security Protocols. - Piergiuseppe Bettassa Copet; Alfredo Pironti 001; Davide Pozza; Riccardo Sisto; Pietro Vivoli (HASE, 2012)

Formally based semi-automatic implementation of an open security protocol. - Alfredo Pironti 001; Davide Pozza; Riccardo Sisto (J. Syst. Softw., 2012)

Implementing TLS with Verified Cryptographic Security. - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub (IEEE Symposium on Security and Privacy, 2013)

Truncating TLS Connections to Violate Beliefs in Web Applications. - Ben Smyth; Alfredo Pironti 001 (WOOT, 2013)

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Alfredo Pironti 001; Pierre-Yves Strub (IEEE Symposium on Security and Privacy, 2014)

Formal verification of security protocol implementations: a survey. - Matteo Avalle; Alfredo Pironti 001; Riccardo Sisto (Formal Aspects Comput., 2014)

Safe abstractions of data encodings in formal security protocol models. - Alfredo Pironti 001; Riccardo Sisto (Formal Aspects Comput., 2014)

Proving the TLS Handshake Secure (as it is). - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2014)

Verified Contributive Channel Bindings for Compound Authentication. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Alfredo Pironti 001 (NDSS, 2015)

FLEXTLS: A Tool for Testing TLS Implementations. - Benjamin Beurdouche; Antoine Delignat-Lavaud; Nadim Kobeissi; Alfredo Pironti 001; Karthikeyan Bhargavan (WOOT, 2015)

Deprecating Secure Sockets Layer Version 3.0. - Richard L. Barnes; Martin Thomson; Alfredo Pironti 001; Adam Langley (RFC, 2015)

Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Alfredo Pironti 001; Adam Langley; Marsh Ray (RFC, 2015)

A messy state of the union: taming the composite state machines of TLS. - Benjamin Beurdouche; Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Jean Karim Zinzindohoue (Commun. ACM, 2017)

Formally sound implementations of security protocols with JavaSPI. - Riccardo Sisto; Piergiuseppe Bettassa Copet; Matteo Avalle; Alfredo Pironti 001 (Formal Aspects Comput., 2018)