Reliable Evidence: Auditability by Typing

  • Nataliya Guts
  • Cédric Fournet
  • Francesco Zappa Nardelli
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5789)


Many protocols rely on audit trails to allow an impartial judge to verify a posteriori some property of a protocol run. However, in current practice the choice of what data to log is left to the programmer’s intuition, and there is no guarantee that it constitutes enough evidence. We give a precise definition of auditability and we show how typechecking can be used to statically verify that a protocol always logs enough evidence. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.


Reliable Evidence Audit Statement Security Goal Evaluation Context Proof Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [Aba99]
    Abadi, M.: Secrecy by typing in security protocols. JACM 46(5), 749–786 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  2. [BBF+08]
    Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: IEEE Computer Security Foundations Symposium, pp. 17–32 (2008)Google Scholar
  3. [BFG08]
    Bhargavan, K., Fournet, C., Gordon, A.D.: F7: Refinement types for F#. version 1.0 (2008),
  4. [BL01]
    Baughman, N.E., Levine, B.N.: Cheat-proof playout for centralized and distributed online games. In: 20th Annual Joint Conference of the IEEE Computer and Communications Societies, vol.1 (2001)Google Scholar
  5. [CCD+07]
    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), 133–151 (2007)CrossRefGoogle Scholar
  6. [EW07]
    Etalle, S., Winsborough, W.H.: A posteriori compliance control. In: SACMAT, pp. 11–20. ACM Press, New York (2007)CrossRefGoogle Scholar
  7. [FGM07]
    Fournet, C., Gordon, A., Maffeis, S.: A Type Discipline for Authorization in Distributed Systems. In: IEEE Computer Security Foundations Symposium, pp. 31–48 (2007)Google Scholar
  8. [FGZN08]
    Fournet, C., Guts, N., Zappa Nardelli, F.: A formal implementation of value commitment. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 383–397. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. [HSW07]
    Hasan, R., Sion, R., Winslett, M.: Introducing secure provenance: problems and challenges. StorageSS (2007)Google Scholar
  10. [ISO04]
    ISO/IEC. Common criteria for information technology security evaluation (2004)Google Scholar
  11. [JVM+08]
    Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: AURA: a programming language for authorization and audit. In: ICFP, pp. 27–38 (2008)Google Scholar
  12. [KMZ02]
    Kremer, S., Markowitch, O., Zhou, J.: An intensive survey of fair non-repudiation protocols. Computer Communications 25(17), 1606–1621 (2002)CrossRefGoogle Scholar
  13. [Pub96]
    NIST Special Publications. Generally accepted principles and practices for securing information technology systems (September 1996)Google Scholar
  14. [Roe97]
    Roe, M.: Cryptography and evidence. PhD thesis, University of Cambridge (1997)Google Scholar
  15. [VJMZ08]
    Vaughan, J.A., Jia, L., Mazurak, K., Zdancewic, S.: Evidence-based audit. In: IEEE Computer Security Foundations Symposium, pp. 177–191 (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Nataliya Guts
    • 1
  • Cédric Fournet
    • 2
    • 1
  • Francesco Zappa Nardelli
    • 3
    • 1
  1. 1.MSR-INRIA Joint CentreFrance
  2. 2.Microsoft ResearchUSA
  3. 3.INRIAFrance

Personalised recommendations