The Internet is such a big part of our lives today that it’s hard to imagine that we once did without it. We use the Internet at work, at home, on the street. We use it to keep in touch, stay on top of the news, research information, manage our savings, pay bills, shop, vote, play and have fun. However, security failures make the news on a regular basis, reminding us that no country, industry, community or individual is immune to cyber risks and we face constant threats against our critical infrastructures, government, economy, identity and privacy.
Experience has shown that the design of protocols and services for Internet security is highly error-prone and that conventional validation techniques based on informal arguments or testing are not up to the task. It is now widely recognised that only formal analysis can provide the level of assurance required by both developers and users. In this talk, I will survey the novel formal methodologies and technologies for information security that he has developed with several collaborators in the context of research and industrial projects, and suggest some interesting directions for the future.