Skip to main content

A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence

  • Conference paper
Formal Methods: Foundations and Applications (SBMF 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6527))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.: The B-Book. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. 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)

    Google Scholar 

  4. Barringer, H., Groce, A., Havelund, K., Smith, M.H.: Formal Analysis of Log Files. Aerospace Computing, Information, and Communication (to appear, 2010)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Buskirk, E.V., Liu, V.T.: Digital Evidence: Challenging the Presumption of Reliability. Journal of Digital Forensic Practice 1(1), 19–26 (2006)

    Article  Google Scholar 

  7. 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)

    Article  Google Scholar 

  8. 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)

    Article  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Grossi, D., Royakkers, L.M.M., Dignum, F.: Organizational Structure and Responsibility. Artificial Intelligence and Law 15(3), 223–249 (2007)

    Article  Google Scholar 

  11. 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)

    Article  MATH  Google Scholar 

  12. 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)

    Article  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  15. 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)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. 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)

    Article  MathSciNet  MATH  Google Scholar 

  18. Maurer, U.M.: New Approaches to Digital Evidence. Proceedings of the IEEE 92(6), 933–947 (2004)

    Article  Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. Saleh, M., Arasteh, A.R., Sakha, A., Debbabi, M.: Forensic Analysis of Logs: Modeling and verification. Knowledge-Based Systems 20(7), 671–682 (2007)

    Article  Google Scholar 

  22. 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)

    Google Scholar 

  23. Schneider, F.B.: Accountability for Perfection. IEEE Security & Privacy 7(2), 3–4 (2009)

    Article  Google Scholar 

  24. Schneier, B., Kelsey, J.: Secure audit logs to support computer forensics. ACM Transactions on Information and System Security 2(2), 159–176 (1999)

    Article  Google Scholar 

  25. Skene, J., Raimondi, F., Emmerich, W.: Service-Level Agreements for Electronic Services. IEEE Transactions on Software Engineering 36(2), 288–304 (2010)

    Article  Google Scholar 

  26. 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)

    Google Scholar 

  27. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics