Formally Reasoning about the Cost and Efficacy of Securing the Email Infrastructure

We propose the first automated methodology for making formal deployment assessments. Our planning algorithm analyses the impact and cost-efficiency of different known mitigation strategies against an attacker in a formal threat model. This novel formalisation of an infrastructure attacker includes routing, name resolution and application level weaknesses. We apply the methodology to a large-scale scan of the Internet, and assess how protocols like IPsec, DNSSEC, DANE, SMTP STS, SMTP over TLS and other mitigation techniques like server relocation can be combined to improve the confidentiality of email users in 45 combinations of attacker and defender countries and nine cost scenarios. This is the first deployment analysis for mitigation techniques at this scale.


Patrick Speicher


Marcel Steinmetz


Robert K√ľnnemann


Milivoj Simeonovski


Giancarlo Pellegrino


Joerg Hoffmann


Michael Backes

# Get to know the research #


The paper was accepted at the European Symposium on Security and Privacy 2018 (EuroS&P'18).


The presentation will be available after the conference (EuroS&P 2018).


Results including all scenarios that were not covered in the paper due to page limit.