Abstract
In this work we model the ACME (a fictitious company name) “printer case incident” and make its specification in Forensic Lucid, a Lucid- and intensional-logic-based programming language for cyberforensic analysis and event reconstruction specification. The printer case involves a dispute between two parties that was previously solved using the finite-state automata (FSA) approach, and is now re-done in a more usable way in Forensic Lucid. Our approach is based on the said case modeling by encoding concepts like evidence and the related witness accounts as an evidential statement context in a Forensic Lucid “program”. The evidential statement is an input to the transition function that models the possible deductions in the case. We then invoke the transition function (actually its reverse) with the evidential statement context to see if the evidence we encoded agrees with one’s claims and then attempt to reconstruct the sequence of events that may explain the claim or disprove it.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Gladyshev, P., Patel, A.: Finite state machine approach to digital event reconstruction. Digital Investigation Journal 2(1) (2004)
Gladyshev, P.: Finite state machine analysis of a blackmail investigation. International Journal of Digital Evidence 4(1) (2005)
Ashcroft, E.A., Wadge, W.W.: Lucid – a formal system for writing and proving programs. SIAM J. Comput. 5(3) (1976)
Ashcroft, E.A., Wadge, W.W.: Erratum: Lucid – a formal system for writing and proving programs. SIAM J. Comput. 6(1), 200 (1977)
Wadge, W.W., Ashcroft, E.A.: Lucid, the Dataflow Programming Language. Academic Press, London (1985)
Ashcroft, E.A., Faustini, A.A., Jagannathan, R., Wadge, W.W.: Multidimensional Programming. Oxford University Press, London (1995) ISBN: 978-0195075977
Lalement, R.: Computation as Logic. Prentice Hall (1993); C.A.R. Hoare Series Editor. English translation from French by John Plaice
Paquet, J.: Distributed eductive execution of hybrid intensional programs. In: Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference (COMPSAC 2009), pp. 218–224. IEEE Computer Society, Seattle (2009)
Plaice, J., Mancilla, B., Ditu, G., Wadge, W.W.: Sequential demand-driven evaluation of eager TransLucid. In: Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), pp. 1266–1271. IEEE Computer Society, Turku (2008)
Rahilly, T., Plaice, J.: A multithreaded implementation for TransLucid. In: Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), pp. 1272–1277. IEEE Computer Society, Turku (2008)
The GIPSY Research and Development Group: The General Intensional Programming System (GIPSY) project. Department of Computer Science and Software Engineering.Concordia University, Montreal (2002–2012), http://newton.cs.concordia.ca/~gipsy/ (last viewed February 2010)
Ding, Y.: Automated translation between graphical and textual representations of intensional programs in the GIPSY. Master’s thesis, Department of Computer Science and Software Engineering. Concordia University, Montreal, Canada (June 2004), http://newton.cs.concordia.ca/~paquet/filetransfer/publications/theses/DingYiminMSc2004.pdf .
Mokhov, S.A., Paquet, J., Debbabi, M.: On the need for data flow graph visualization of Forensic Lucid programs and forensic evidence, and their evaluation by GIPSY. In: Proceedings of the Ninth Annual International Conference on Privacy, Security and Trust (PST), pp. 120–123. IEEE Computer Society (July 2011) Short paper; full version online at http://arxiv.org/abs/1009.5423
Ji, Y.: Scalability evaluation of the GIPSY runtime system. Master’s thesis, Department of Computer Science and Software Engineering. Concordia University, Montreal, Canada (March 2011)
Mokhov, S.A.: Enhancing the formal cyberforensic approach with observation modeling with credibility factors and mathematical theory of evidence. Login 34(6), 101 (2009); Presented at WIPS at USENIX Security 2009, http://www.usenix.org/events/sec09/wips.html
Mokhov, S.A., Paquet, J., Debbabi, M.: Towards automated deduction in blackmail case analysis with Forensic Lucid. In: Gauthier, J.S. (ed.) Proceedings of the Huntsville Simulation Conference (HSC 2009). SCS, pp. 326–333 (October 2009), http://arxiv.org/abs/0906.0049
Mokhov, S.A.: The role of self-forensics modeling for vehicle crash investigations and event reconstruction simulation. In: Gauthier, J.S. (ed.) Proceedings of the Huntsville Simulation Conference (HSC 2009). SCS, pp. 342–349 (October 2009), http://arxiv.org/abs/0905.2449
Mokhov, S.A., Paquet, J., Debbabi, M.: Formally specifying operational semantics and language constructs of Forensic Lucid. In: Göbel, O., Frings, S., Günther, D., Nedon, J., Schadt, D. (eds.) Proceedings of the IT Incident Management and IT Forensics (IMF 2008). LNI, vol. 140, pp. 197–216. GI (September 2008)
Mokhov, S.A., Paquet, J.: Formally specifying and proving operational aspects of Forensic Lucid in Isabelle. Technical Report 2008-1-Ait Mohamed, Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada. In: Theorem Proving in Higher Order Logics (TPHOLs 2008): Emerging Trends Proceedings (August 2008)
Paquet, J.: Scientific Intensional Programming. PhD thesis, Department of Computer Science. Laval University, Sainte-Foy, Canada (1999)
Ashcroft, E.A., Wadge, W.W.: Lucid, a nonprocedural language with iteration. Communications of the ACM 20(7), 519–526 (1977)
Tong, X.: Design and implementation of context calculus in the GIPSY. Master’s thesis, Department of Computer Science and Software Engineering. Concordia University, Montreal, Canada (April 2008)
Wan, K.: Lucx: Lucid Enriched with Context. PhD thesis, Department of Computer Science and Software Engineering.Concordia University, Montreal, Canada (2006)
Mokhov, S.A.: Towards syntax and semantics of hierarchical contexts in multimedia processing applications using MARFL. In: Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), pp. 1288–1294. IEEE Computer Society, Turku (2008)
Riley, G.: CLIPS: A tool for building expert systems (2007-2009), http://clipsrules.sourceforge.net/ (last viewed: October 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 ICST Institute for Computer Science, Social Informatics and Telecommunications Engineering
About this paper
Cite this paper
Mokhov, S.A., Paquet, J., Debbabi, M. (2012). Reasoning About a Simulated Printer Case Investigation with Forensic Lucid. In: Gladyshev, P., Rogers, M.K. (eds) Digital Forensics and Cyber Crime. ICDF2C 2011. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol 88. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35515-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-35515-8_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35514-1
Online ISBN: 978-3-642-35515-8
eBook Packages: Computer ScienceComputer Science (R0)