Automated Formal Methods for Security Protocol Engineering

Automated Formal Methods for Security Protocol Engineering

Alfredo Pironti (Politecnico di Torino, Italy), Davide Pozza (Politecnico di Torino, Italy) and Riccardo Sisto (Politecnico di Torino, Italy)
DOI: 10.4018/978-1-60960-851-4.ch008


Designing and implementing security protocols are known to be error-prone tasks. Recent research progress in the field of formal methods applied to security protocols has enabled the use of these techniques in practice. The objective of this chapter is to give a circumstantial account of the state-of-the-art reached in this field, showing how formal methods can help in improving quality. Since automation is a key factor for the acceptability of these techniques in the engineering practice, the chapter focuses on automated techniques and illustrates in particular how high-level protocol models in the Dolev-Yao style can be automatically analyzed and how it is possible to automatically enforce formal correspondence between an abstract high-level model and an implementation.
Chapter Preview


A security protocol can be defined as a communication protocol aimed at reaching a goal in a distributed environment even in the presence of hostile agents that have access to the network. Examples of security goals are user authentication (that is, proving a user’s identity to another remote user) and secrecy in data exchange (that is, transferring data in such a way that only the intended recipients can read transmitted data).

Complete Chapter List

Search this Book: