Security models in rewriting logic for cryptographic protocols and browsers

browser security;visual invariants;same origin policy;semantic unification;variant narrowing;cryptographic protocol analysis;rewriting logic

Sasse, Ralf

关键词: browser security;    visual invariants;    same origin policy;    semantic unification;    variant narrowing;    cryptographic protocol analysis;    rewriting logic;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/34373/sasse_ralf.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

This dissertation tackles crucial issues of web browser security. Webbrowsers are now a central part of the trusted code base of anyend-user computer system, as more and more usage shifts to servicesprovided by web sites that are accessed through thosebrowsers. Towards this goal we identify three key aspects of webbrowser security: (i) the \emph{machine-to-user communication}, (ii)\emph{internal browser security concerns} and (iii)\emph{machine-to-machine communication}.We address aspects (i) and (ii) by developing a methodology thatcreates a formal model of a web browser and analyzes that model. Weshowcase this on the graphical user interface of both InternetExplorer and the Illinois Browser Operating System (IBOS) webbrowsers. Internal security aspects are addressed in the IBOS browserfor the same origin policy.For aspect (iii) we look at the formal analysis of cryptographicprotocols, independent of any particular browser.We focus on theformal analysis of protocols \emph{modulo algebraic properties} oftheir cryptographic functions, since it is well-known the protocolverification methods that ignore such algebraic properties using astandard Dolev-Yao model can verify as correct protocols that can bein fact broken using the algebraic properties. We adopt a symbolicapproach and use the Maude-NPA cryptographic protocol analysis tool,which has extended unification capabilities modulo theories based onthe new narrowing strategy we developed. We present case studiesshowing that appropriate protocols can be analyzed so that eitherattacks are found, or the absence of attacks can be proven.