Intensional Cyberforensics

Doctoral dissertation
Concordia University
digital forensics, digital investigation, Forensic Lucid, intensional logic, intensional programming, formal methods, event reconstruction, Dempster-Shafer theory of evidence, GIPSY, MARF

This work focuses on the application of intensional logic to cyberforensic analysis and its benefits and difficulties are compared with the previous finite-state-automata (FSA) approach. This work extends the use of the intensional programming paradigm to the modeling and implementation of a digital forensics investigation process with backtracing of event reconstruction, in which evidence is modeled by multidimensional hierarchical contexts, and proofs or disproofs of claims are undertaken in an eductive manner of evaluation. This approach is a practical, context-aware improvement over the FSA approach we have seen in previous work. As a base implementation language model, we use in this approach a new dialect of the Lucid programming language, called Forensic Lucid, and we focus on defining hierarchical contexts based on intensional logic for the distributed evaluation of cyberforensic expressions. We also augment the work with credibility factors surrounding digital evidence and witness accounts, which have not been previously modeled. The Forensic Lucid programming language, used for this intensional cyberforensic analysis, is formally presented through its syntax and operational semantics.