An algebraic framework for reasoning about privacy
Thesis (PhD)--Stellenbosch University, 2016.
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 refine-ment 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.
AFRIKAANSE OPSOMMING : Geen Afrikaanse opsomming geskikbaar nie.