{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/34373"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/34373","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Security models in rewriting logic for cryptographic protocols and browsers","abstract":"This dissertation tackles crucial issues of web browser security. Web browsers are now a central part of the trusted code base of any end-user computer system, as more and more usage shifts to services provided by web sites that are accessed through those browsers. Towards this goal we identify three key aspects of web browser 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 that creates a formal model of a web browser and analyzes that model. We showcase this on the graphical user interface of both Internet Explorer and the Illinois Browser Operating System (IBOS) web browsers. Internal security aspects are addressed in the IBOS browser for the same origin policy. For aspect (iii) we look at the formal analysis of cryptographic protocols, independent of any particular browser. We focus on the formal analysis of protocols \\emph{modulo algebraic properties} of their cryptographic functions, since it is well-known the protocol verification methods that ignore such algebraic properties using a standard Dolev-Yao model can verify as correct protocols that can be in fact broken using the algebraic properties. We adopt a symbolic approach and use the Maude-NPA cryptographic protocol analysis tool, which has extended unification capabilities modulo theories based on the new narrowing strategy we developed. We present case studies showing that appropriate protocols can be analyzed so that either attacks are found, or the absence of attacks can be proven.","abstract_html":"This dissertation tackles crucial issues of web browser security. Web browsers are now a central part of the trusted code base of any end-user computer system, as more and more usage shifts to services provided by web sites that are accessed through those browsers. Towards this goal we identify three key aspects of web browser 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 that creates a formal model of a web browser and analyzes that model. We showcase this on the graphical user interface of both Internet Explorer and the Illinois Browser Operating System (IBOS) web browsers. Internal security aspects are addressed in the IBOS browser for the same origin policy. For aspect (iii) we look at the formal analysis of cryptographic protocols, independent of any particular browser. We focus on the formal analysis of protocols \\emph{modulo algebraic properties} of their cryptographic functions, since it is well-known the protocol verification methods that ignore such algebraic properties using a standard Dolev-Yao model can verify as correct protocols that can be in fact broken using the algebraic properties. We adopt a symbolic approach and use the Maude-NPA cryptographic protocol analysis tool, which has extended unification capabilities modulo theories based on the new narrowing strategy we developed. We present case studies showing that appropriate protocols can be analyzed so that either attacks are found, or the absence of attacks can be proven.","abstract_has_math":false,"creators":["Sasse, Ralf"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","King, Samuel T.","Roşu, Grigore","Meadows, Catherine","Chen, Shuo"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-09-18T21:13:51Z","date_published":"2012-09-18T21:13:51Z","updated_at":"2026-07-22T22:25:31Z","subjects":["rewriting logic","browser security","visual invariants","same origin policy","semantic unification","variant narrowing","cryptographic protocol analysis"],"languages":["en"],"rights":["Copyright 2012 Ralf Sasse"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/34373","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","King, Samuel T.","Roşu, Grigore","Meadows, Catherine","Chen, Shuo"]},{"key":"dc:creator","label":"Author","values":["Sasse, Ralf"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2012-09-18T21:13:51Z","2012-08"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["rewriting logic","browser security","visual invariants","same origin policy","semantic unification","variant narrowing","cryptographic protocol analysis"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2012 Ralf Sasse"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/34373"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This dissertation tackles crucial issues of web browser security. Web browsers are now a central part of the trusted code base of any end-user computer system, as more and more usage shifts to services provided by web sites that are accessed through those browsers. Towards this goal we identify three key aspects of web browser 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 that creates a formal model of a web browser and analyzes that model. We showcase this on the graphical user interface of both Internet Explorer and the Illinois Browser Operating System (IBOS) web browsers. Internal security aspects are addressed in the IBOS browser for the same origin policy. For aspect (iii) we look at the formal analysis of cryptographic protocols, independent of any particular browser. We focus on the formal analysis of protocols \\emph{modulo algebraic properties} of their cryptographic functions, since it is well-known the protocol verification methods that ignore such algebraic properties using a standard Dolev-Yao model can verify as correct protocols that can be in fact broken using the algebraic properties. We adopt a symbolic approach and use the Maude-NPA cryptographic protocol analysis tool, which has extended unification capabilities modulo theories based on the new narrowing strategy we developed. We present case studies showing that appropriate protocols can be analyzed so that either attacks are found, or the absence of attacks can be proven.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-07-05T16:00:06Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 sasse_ralf.zip: 4933492 bytes, checksum: d26e593661e755392bbc0dfc651f5e6f (MD5) sasse_ralf.pdf: 1940240 bytes, checksum: 5cfe2010afd635b3162c315e2bcff64a (MD5)","Made available in DSpace on 2012-09-18T21:13:51Z (GMT). No. of bitstreams: 3 sasse_ralf.pdf: 1940240 bytes, checksum: 5cfe2010afd635b3162c315e2bcff64a (MD5) license.txt: 4058 bytes, checksum: 92c2f890d09f42a359461c43e5c3e564 (MD5) sasse_ralf.zip: 4933492 bytes, checksum: d26e593661e755392bbc0dfc651f5e6f (MD5)"]},{"key":"dc:title","label":"Title","values":["Security models in rewriting logic for cryptographic protocols and browsers"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","King, Samuel T.","Roşu, Grigore","Meadows, Catherine","Chen, Shuo"],"dc:creator":["Sasse, Ralf"],"dc:date":["2012-09-18T21:13:51Z","2012-08"],"dc:description":["This dissertation tackles crucial issues of web browser security. Web browsers are now a central part of the trusted code base of any end-user computer system, as more and more usage shifts to services provided by web sites that are accessed through those browsers. Towards this goal we identify three key aspects of web browser 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 that creates a formal model of a web browser and analyzes that model. We showcase this on the graphical user interface of both Internet Explorer and the Illinois Browser Operating System (IBOS) web browsers. Internal security aspects are addressed in the IBOS browser for the same origin policy. For aspect (iii) we look at the formal analysis of cryptographic protocols, independent of any particular browser. We focus on the formal analysis of protocols \\emph{modulo algebraic properties} of their cryptographic functions, since it is well-known the protocol verification methods that ignore such algebraic properties using a standard Dolev-Yao model can verify as correct protocols that can be in fact broken using the algebraic properties. We adopt a symbolic approach and use the Maude-NPA cryptographic protocol analysis tool, which has extended unification capabilities modulo theories based on the new narrowing strategy we developed. We present case studies showing that appropriate protocols can be analyzed so that either attacks are found, or the absence of attacks can be proven.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-07-05T16:00:06Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 sasse_ralf.zip: 4933492 bytes, checksum: d26e593661e755392bbc0dfc651f5e6f (MD5) sasse_ralf.pdf: 1940240 bytes, checksum: 5cfe2010afd635b3162c315e2bcff64a (MD5)","Made available in DSpace on 2012-09-18T21:13:51Z (GMT). No. of bitstreams: 3 sasse_ralf.pdf: 1940240 bytes, checksum: 5cfe2010afd635b3162c315e2bcff64a (MD5) license.txt: 4058 bytes, checksum: 92c2f890d09f42a359461c43e5c3e564 (MD5) sasse_ralf.zip: 4933492 bytes, checksum: d26e593661e755392bbc0dfc651f5e6f (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/34373"],"dc:language":["en"],"dc:rights":["Copyright 2012 Ralf Sasse"],"dc:subject":["rewriting logic","browser security","visual invariants","same origin policy","semantic unification","variant narrowing","cryptographic protocol analysis"],"dc:title":["Security models in rewriting logic for cryptographic protocols and browsers"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:31Z"}