The aim of the Pesto project is to build formal models and techniques, for computer-aided analysis and design of security protocols (in a broad sense). While historically the main goals of protocols were condentiality and authentication the situation has changed. E-voting protocols need to guarantee privacy of votes, while ensuring transparency of the election; electronic devices communicate data by the means of web services; RFID and mobile phone protocols have to guarantee that people cannot be traced. Due to malware, security protocols need to rely on additional mechanisms, such as trusted hardware components or multi-factor authentication, to guarantee security even if the computing platform is a priori untrusted. Current existing techniques and tools are however unable to analyse the properties required by these new protocols and take into account the newly deployed mechanisms and associated attacker models.