An algebraic framework for reasoning about privacy
Date
2016-03
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : University of Stellenbosch
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.
AFRIKAANSE OPSOMMING : Geen Afrikaanse opsomming beskikbaar nie.
AFRIKAANSE OPSOMMING : Geen Afrikaanse opsomming beskikbaar nie.
Description
Thesis (PhD)--Stellenbosch University, 2016.
Keywords
Algebraic techniques, Program verification, Programming languages, Programming (Computers), Refinement (Computing), Semantics (Computer science), Security protocols (Programming)