On the Automated Correction of Security Protocols Susceptible to a Replay Attack

On the Automated Correction of Security Protocols Susceptible to a Replay Attack

Dr. Raúl Monroy

Texto completo de la Conferencia   

Although there exist informal design guidelines and formal development support, security protocol development is time-consuming because design is error-prone. In this talk, we introduce Shrimp, a mechanism that aims to speed up the development cycle by adding automated aid for protocol diagnosis and repair. Shrimp relies on existing verification tools both to analyse an intermediate protocol and to compute attacks if the protocol is flawed. Then it analyses such attacks to pinpoint the source of the failure and synthesises appropriate patches, using Abadi and Needham's principles for protocol design. We have translated some of these principles into formal requirements on (sets of) protocol steps. For each requirement, there is a collection of rules that transform a set of protocol steps violating the requirement into a set conforming it. We have successfully tested our mechanism on 36 faulty protocols, getting a repair rate of 90%.

Esbozo Curricular

Raúl Monroy obtained a PhD in Artificial Intelligence in 1998 from Edinburgh University, under the supervision of Prof. Alan Bundy. He has been in Computing at Tecnológico de Monterrey (ITESM), Campus Estado de México, since 1985. In 1992 he was promoted to Assistant Professor and in 2000 he was promoted to Associate Professor. Since 1998 he is a member of the CONACYT-SNI National Research System.

Dr. Monroy's research focuses on automating the application of theorem proving to formal methods of system development. He is also interested in issues of computer security. Currently, his research concerns: the discovery and application of proof plans to automate the verification of security protocols; the discovery an application of general search control strategies for uncovering and correcting errors in either a system or its specification; the discovery of novel methods for anomaly detection in computer security; and motion planning.

Dr. Monroy has held 6 research grants from several funding agencies, including CONACYT (holder), the national research council,  BMBF (co-holder), FRIDA (holder) and CONACyT-REDII (co-holder) and is the sole or joint author of over 30 published papers. He is programme co-chair for MICAI-2004 and MICAI-2005 and serves on the programme committee of various AI conferences. He has been Secretary Treasurer to the Mexican Society for Artificial Intelligence since 2000.