Socio-technical formal analysis of TLS certificate validation in modern browsers

Interdisciplinary Research Group in Socio-technical Cybersecurity

Socio-technical formal analysis of TLS certificate validation in modern browsers

Bella, Giampaolo, Giustolisi Rosario, Lenzini Gabriele
Abstract:
Authenticating a web server is crucial to the security of web browsing. It relies on TLS certificate validation, a property whose enforcement may require getting the user involved. Thus, certificate validation is a socio-technical property - it relies on traditional security technology as well as on social elements such as cultural values, trust and human-computer interaction. Hence the need for an appropriate methodology to study certificate validation from a socio-technical perspective. Certificate validation as carried out through today's most popular browsers - Chrome, Internet Explorer, Firefox and Opera Mini - is first represented by means of UML activity diagrams. It is then translated into CSP#, and expanded with the LTL formalization of four socio-technical properties pivoted on user involvement with certificate validation. The properties are then checked automatically using the PAT model checker. The findings turn out to be far from straightforward and, most importantly, allowed for prototyping a basic methodology for the sociotechnical formal analysis of security properties.
Authors:
Bella, Giampaolo, Giustolisi Rosario, Lenzini Gabriele
Publication date:
2013
Published in:
2013 Eleventh Annual Conference on Privacy, Security and Trust
Reference:
Bella, G., Giustolisi, R., & Lenzini, G. (2013, July). Socio-technical formal analysis of TLS certificate validation in modern browsers. In 2013 Eleventh Annual Conference on Privacy, Security and Trust (pp. 309-316). IEEE.

Get in touch with us

SnT – Interdisciplinary Centre for Security, Reliability and Trust
29, Avenue J.F Kennedy L-1855 Luxembourg
info-irisc-lab@uni.lu