A Lightweight Formal Approach for Analyzing Security of Web Protocols

摘要: Existing model checking tools for cryptographic protocol analysis have two drawbacks, when applied to present day web based protocols. Firstly, they require expertise in specialized formalisms which limits their use a small fragment of scientific community. Secondly, do not support common constructs and attacks making the both cumbersome as well error-prone. In this paper, we propose novel security technique We provide explicit mechanisms an adversary capable exploiting browser-based interaction. Our approach has unique aspects. It represents only tool built using general purpose first-order logic modeling language – Alloy that can be used analyze industrial strength The other aspect is our inference system analyzes beliefs at honest participants simplify model. Despite its simplicity, demonstrate effectiveness through case-study SAML, where identify previously unknown vulnerability identity federation workflow.