Abstract
The issues of logging for determining liability requires to define, prior to a dispute, the logging system and the log analysis in a manner that would determine the parties liable for a predetermined misbehavior of the system. We propose a formal framework for specifying and reasoning about decentralized logs to be used in legal disputes. In addition, we study how previous results can be used in the incremental analysis of larger inputs to obtain precise or approximated results. We illustrate our approach with an example of a travel arrangement service.
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
Abrial, J.: The B-Book. Cambridge University Press, Cambridge (1996)
Badeau, F., Amelot, A.: Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334–354. Springer, Heidelberg (2005)
Barringer, H., Groce, A., Havelund, K., Smith, M.H.: An Entry Point for Formal Methods: Specification and Analysis of Event Logs. CoRR abs/1003.1682 (2010)
Barringer, H., Groce, A., Havelund, K., Smith, M.H.: Formal Analysis of Log Files. Aerospace Computing, Information, and Communication (to appear, 2010)
Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: A Successful Application of B in a Large Project. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999)
Buskirk, E.V., Liu, V.T.: Digital Evidence: Challenging the Presumption of Reliability. Journal of Digital Forensic Practice 1(1), 19–26 (2006)
Cederquist, J.G., Corin, R., Dekker, M.A.C., Etalle, S., den Hartog, J.I., Lenzini, G.: Audit-based Compliance Control. International Journal of Information Security 6(2-3), 133–151 (2007)
Farrell, A.D.H., Sergot, M.J., Sallé, M., Bartolini, C.: Using the Event Calculus for Tracking the Normative State of Contracts. International Journal of Cooperative Information Systems (IJCIS) 14(2-3), 99–129 (2005)
Fenech, S., Pace, G.J., Schneider, G.: CLAN: A tool for contract analysis and conflict discovery. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 90–96. Springer, Heidelberg (2009)
Grossi, D., Royakkers, L.M.M., Dignum, F.: Organizational Structure and Responsibility. Artificial Intelligence and Law 15(3), 223–249 (2007)
Hallal, H., Boroday, S., Petrenko, A., Ulrich, A.: A Formal Approach to Property Testing in Causally Consistent Distributed Traces. Formal Aspects of Computing 18(1), 63–83 (2006)
Insa, F.: The Admissibility of Electronic Evidence in Court (AEEC): Fighting against High-Tech Crime - Results of a European Study. Journal of Digital Forensic Practice 1(4), 285–289 (2006)
Kyas, M., Prisacariu, C., Schneider, G.: Run-Time Monitoring of Electronic Contracts. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 397–407. Springer, Heidelberg (2008)
Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558–565 (1978)
Le Métayer, D., Maarek, M., Mazza, E., Potet, M.L., Viet Triem Tong, V., Craipeau, N., Frénot, S., Hardouin, R.: Liability in Software Engineering: Overview of the LISE Approach and Illustration on a Case Study. In: International Conference on Software Engineering (ICSE), pp. 135–144 (2010)
Le Métayer, D., Mazza, E., Potet, M.L.: Designing Log Architecture For Legal Evidence. In: Software Engineering And Formal Methods (SEFM). IEEE, Los Alamitos (2010)
Lima, T.D., Royakkers, L.M.M., Dignum, F.: A Logic For Reasoning About Responsibility. Logic Journal of the IGPL 18(1), 99–117 (2010)
Maurer, U.M.: New Approaches to Digital Evidence. Proceedings of the IEEE 92(6), 933–947 (2004)
Peisert, S., Bishop, M., Karin, S., Marzullo, K.: Toward Models for Forensic Analysis. In: Systematic Approaches to Digital Forensic Engineering, pp. 3–15. IEEE, Los Alamitos (2007)
Rekhis, S., Krichène, J., Boudriga, N.: Cognitive-Maps Based Investigation of Digital Security Incidents. In: Systematic Approaches to Digital Forensic Engineering, pp. 25–40 (2008)
Saleh, M., Arasteh, A.R., Sakha, A., Debbabi, M.: Forensic Analysis of Logs: Modeling and verification. Knowledge-Based Systems 20(7), 671–682 (2007)
Sandler, D., Derr, K., Crosby, S.A., Wallach, D.S.: Finding the Evidence in Tamper-Evident Logs. In: Systematic Approaches to Digital Forensic Engineering, pp. 69–75 (2008)
Schneider, F.B.: Accountability for Perfection. IEEE Security & Privacy 7(2), 3–4 (2009)
Schneier, B., Kelsey, J.: Secure audit logs to support computer forensics. ACM Transactions on Information and System Security 2(2), 159–176 (1999)
Skene, J., Raimondi, F., Emmerich, W.: Service-Level Agreements for Electronic Services. IEEE Transactions on Software Engineering 36(2), 288–304 (2010)
Stirewalt, R.E.K., Dillon, L.K., Kraemer, E.: The Inference Validity Problem in Legal Discovery. In: International Conference on Software Engineering (ICSE), pp. 303–306. IEEE, Los Alamitos (2009)
Waters, B.R., Balfanz, D., Durfee, G., Smetters, D.K.: Building an Encrypted and Searchable Audit Log. In: Proceedings of the Network and Distributed System Security. The Internet Society (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mazza, E., Potet, ML., Le Métayer, D. (2011). A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence. In: Davies, J., Silva, L., Simao, A. (eds) Formal Methods: Foundations and Applications. SBMF 2010. Lecture Notes in Computer Science, vol 6527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19829-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-19829-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19828-1
Online ISBN: 978-3-642-19829-8
eBook Packages: Computer ScienceComputer Science (R0)