An algebraic framework for reasoning about privacy
dc.contributor.advisor | Sanders, J. W. | en_ZA |
dc.contributor.author | Rajaona, Solofomampionona Forunat | en_ZA |
dc.contributor.other | Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Mathematics. | en_ZA |
dc.date.accessioned | 2019-10-09T08:09:27Z | |
dc.date.available | 2019-10-09T08:09:27Z | |
dc.date.issued | 2016-03 | |
dc.description | Thesis (PhD)--Stellenbosch University, 2016. | en_ZA |
dc.description.abstract | ENGLISH ABSTRACT: In this thesis, we study a formal programming language and algebraic tech-niques to analyse computational systems that considers data confidentiality and hidden computations. The reasoning techniques are based on the refinement of programs (Back and von Wright, Carroll Morgan). The underlying logic is a first-order S 5 n epistemic logic that distinguish b etween o bjects and concepts – of the family of Melvin Fitting’s First Order Intensional Logic. We give a relational semantics and a weakest-precondition semantics to prove the soundness of programming laws. The laws for confidentiality r efinement ex-tends those of Carroll Morgan’s Shadow Knows refinement c alculus, whereas the laws for reasoning about knowledge derives mostly from the Public An-nouncement Logic. As applications for knowledge dynamics, we study the classical puzzles of the Three Wise Men and the Muddy Children by means of the programming laws; and as an application for reasoning about confiden-tiality and anonymity, we give a sketch of formal analysis of the Anonymous Cocaine Auction Protocol. | en_ZA |
dc.description.abstract | AFRIKAANSE OPSOMMING : Geen Afrikaanse opsomming beskikbaar nie. | af_ZA |
dc.format.extent | vi, 104 pages | en_ZA |
dc.identifier.uri | http://hdl.handle.net/10019.1/106607 | |
dc.language.iso | en_ZA | en_ZA |
dc.publisher | Stellenbosch : University of Stellenbosch | en_ZA |
dc.rights.holder | University of Stellenbosch | en_ZA |
dc.subject | Algebraic techniques | en_ZA |
dc.subject | Program verification | en_ZA |
dc.subject | Programming languages | en_ZA |
dc.subject | Programming (Computers) | en_ZA |
dc.subject | Refinement (Computing) | en_ZA |
dc.subject | Semantics (Computer science) | en_ZA |
dc.subject | Security protocols (Programming) | en_ZA |
dc.title | An algebraic framework for reasoning about privacy | en_ZA |
dc.type | Thesis | en_ZA |