Non-repudiation analysis using LySa with annotations

https://doi.org/10.1016/j.cl.2010.04.002Get rights and content

Abstract

This work introduces a formal analysis of the non-repudiation property for security protocols. Protocols are modelled in the process calculus LySa, using an extended syntax with annotations. Non-repudiation is verified using a Control Flow Analysis, following the same approach of Buchholtz and Gao for authentication and freshness analyses.

The result is an analysis that can statically check the protocols to predict if they are secure during their execution and which can be fully automated.

Introduction

With the growth of Internet applications like e-shopping or e-voting, non-repudiation is becoming increasingly important, as a protocol property. Our aim is to provide a protocol analysis which checks this property to avoid that a protocol is used in malicious way. Among the existing techniques that perform the analysis of non-repudiation protocols, we may cite:

  • The CSP (Communicating Sequential Processes) approach [14], [15], [16]: it is an abstract language designed specifically for the description of communication patterns of concurrent system components that interact through message passing.

  • The game approach [12]: it considers the execution of the protocol as a game, where each entity is a player; the protocols are designed finding a strategy, which has to defend an honest entity against all the possible strategies of malicious parties.

  • The Zhou–Gollmann approach [19]: it uses SVO Logic, a modal logic that is composed by inference rules and axioms which are used to express beliefs that can be analysed by a judge to decide if the service provided the property.

  • The inductive approach [1]: it uses an inductive model, a set of all the possible histories of the network that the protocol execution may produce; a history, called trace, is a list of network events, that can indicate the communication of a message or the annotation of information for future use.

We follow a different approach, the same as Buchholtz [4] and Gao [7], who show how some security properties can be analysed using the LySa [2] process calculus with annotations and a Control Flow Analysis (CFA) to detect flaws in the protocols. The main idea is to extend LySa with specific annotations, i.e. tags that identify part of the message for which the property has to hold and that uniquely assigns principal identifiers and session identifiers to encryptions and decryptions.

The advantages of this proposal are the following:

  • The analysis is general enough to check any protocol (even if in few exceptional cases the result can be incorrect).

  • The environment in which the protocol is executed can possibly involve infinitely many principals who run infinitely many sessions.

  • The analysis can easily be implemented, providing a user-friendly tool which can automatically check the non-repudiation property for any specified encoding.

It is interesting to notice that the non-repudiation analysis that we propose easily fits into the CFA framework [13], yielding a suite of analyses that can be combined in various ways, with no major implementation overload. Since the analyses share the same framework differing only in the annotations, a combination of them might lead to a result with less resource consumption. This combination could be easily obtained by generalizing the syntax and turning the correspondent monitors on in the semantics.

The structure of the paper is the following: Section 2 is a quick overview of LySa; Section 3 presents the CFA framework; Section 4 shows the new non-repudiation analysis, and its application to the protocols; Section 5 concludes.

Section snippets

LySa

LySa [2] is a process calculus in the π-calculus tradition that models security protocols on a global network. It incorporates pattern matching into the language constructs where values can become bound to variables. In LySa all the communications take place directly on a global network and this corresponds to the scenario in which security protocols often operate. Channels are considered in many process calculi, but they may give a degree of security that there is not in the common network,

Control flow analysis

In this section we introduce our Control Flow Analysis (CFA) as an extension of [13]. The aim of the CFA is to collect information about the behavior of a process and to store them in some data structures A, called analysis components. To be finite, static analysis is forced to compute approximations rather than exact answers. Therefore the analysis can give false positives but it has to preserve soundness.

We will use Flow Logic settings for the specification and the proofs. It is a formalism

Non-repudiation analysis

Non-repudiation guarantees that the principals exchanging messages cannot falsely deny having sent or received the messages. This is done using evidences [11] that allow to decide unquestionably in favor of the fair principal whenever there is a dispute. In particular, non-repudiation of origin provides the recipient with proof of origin while non-repudiation of receipt provides the originator with proof of receipt. Evidences [18] should have verifiable origin, integrity and validity.

The syntax

Conclusions and future works

This paper extends the work by Buchholtz and Gao who defined a suite of analyses for security protocols, namely authentication, confidentiality [10], freshness [9], simple [3] and complex [8] type flaws. The annotations we introduce allow to express non-repudiation also for part of the message: this allows to tune the analysis focussing on relevant components. It results that the CFA framework developed for the process calculus LySa can be extended to security properties by identifying suitable

Acknowledgments

Work partially supported by MIUR Project PRIN 2007 “SOFT” and by RAS Project TESLA—Tecniche di enforcement per la sicurezza dei linguaggi e delle applicazioni.

References (19)

  • J. Zhou et al.

    Evidence and non-repudiation

    J Network Comput Appl

    (1997)
  • Bella G, Paulson LC. Mechanical proofs about a non-repudiation protocol. In: TPHOL’01, Lecture notes in computer...
  • Bodei C, Buchholtz M, Degano P, Nielson F, Nielson HR. Static validation of security protocols. J Comput Security...
  • Bodei C, Degano P, Gao H, Brodo L. Detecting and preventing type flaws: a control flow analysis with tags. In:...
  • Buchholtz M, Lyngby K. Automated analysis of security in networking systems. PhD thesis proposal. Available from...
  • Cederquist J, Corin R, Torabi Dashti M. On the quest for impartiality: design and analysis of a fair non-repudiation...
  • Dolev D, Yao AC. On the security of public key protocols. Technical Report, Stanford, CA;...
  • Gao H. Analysis of protocols by annotations. PhD thesis, Informatics and Mathematical Modelling, Technical University...
  • Gao H, Bodei C, Degano, P. A formal analysis of complex type flaw attacks on security protocols. In: Proceeding of 12th...
There are more references available in the full text version of this article.

Cited by (0)

View full text