Security protocol specification and verification with AnBx

Article English OPEN
Bugliesi, Michele ; Calzavara, Stefano ; Mödersheim, Sebastian Alexander ; Modesti, Paolo (2016)
  • Publisher: Elsevier Advanced Technology
  • Related identifiers: doi: 10.1016/j.jisa.2016.05.004
  • Subject: sub_programming | Protocol verification | Model-checking | sub_networkcomputing | Cybersecurity | e-payment | Protocol specification

Designing distributed protocols is complex and requires actions at very different levels: from the design of an interaction flow supporting the desired application-specific guarantees, to the selection of the most appropriate network-level protection mechanisms.\ud To tame this complexity, we propose AnBx, a formal protocol specification language based on the popular Alice & Bob notation. AnBx offers channels as the main abstraction for communication, providing different authenticity and/or confidentiality guarantees for message transmission.\ud AnBx extends existing proposals in the literature with a novel notion of forwarding channels, enforcing specific security guarantees from the message originator to the final recipient along a number of intermediate forwarding agents. We give a formal semantics of AnBx in terms of a state transition system expressed in the AVISPA Intermediate Format. We devise an ideal channel model\ud and a possible cryptographic implementation, and we show that, under mild restrictions, the two representations coincide, thus making AnBx amenable to automated verification with different tools. We demonstrate the benefits of the declarative specification style distinctive of AnBx by revisiting the design of two existing e-payment protocols, iKP and SET.
  • References (39)
    39 references, page 1 of 4

    [1] G. Lowe, Casper: a compiler for the analysis of security protocols, Journal of Computer Security 6 (1) (1998) 53-84.

    [2] G. Denker, J. Millen, H. Rueß, The CAPSL integrated protocol environment, Tech. Rep. SRI-CSL-2000-02, SRI International, Menlo Park, CA (2000).

    [3] F. Jacquemard, M. Rusinowitch, L. Vigneron, Compiling and verifying security protocols, in: LPAR'00, LNCS 1955, 2000, pp. 131-160.

    [4] S. Mo¨dersheim, Algebraic Properties in Alice and Bob Notation, in: ARES'09, 2009, pp. 433-440.

    [5] Y. Chevalier, M. Rusinowitch, Compiling and securing cryptographic protocols, Information Processing Letters 110 (3) (2010) 116 - 122.

    [6] O. Almousa, S. Mo¨dersheim, L. Vigan`o, Alice and Bob: Reconciling formal models and implementation, in: Programming Languages with Applications to Biology and Security, Vol. 9465 of LNCS, 2015, pp. 66-85.

    [7] U. Carlsen, Generating formal crypto- [20] A. Kamil, G. Lowe, Specifying and modgraphic protocol specifications, in: IEEE elling secure channels in strand spaces, in: S&P'94, 1994, pp. 137-146. FAST'09, 2009.

    [8] J. Millen, F. Muller, Cryptographic pro- [21] A. Kamil, G. Lowe, Understanding abtocol generation from CAPSL, Tech. Rep. stractions of secure channels, in: FAST'11, SRI-CSL-01-07, SRI International (2001). Springer, 2011, pp. 50-64.

    [9] M. Jakobsson, K. Sako, R. Impagliazzo, [22] S. Mo¨dersheim, L. Vigan`o, Secure Designated verifier proofs and their appli- pseudonymous channels, in: M. Backes, cations, in: EUROCRYPT'96, 1996, pp. P. Ning (Eds.), ESORICS'09, Vol. 5789 of 143-158. LNCS, Springer, 2009, pp. 337-354.

    [10] J. N. Quaresma, C. W. Probst, Protocol [23] S. Mo¨dersheim, L. Vigan`o, Sufficient conimplementation generator, in: NordSec'10, ditions for vertical composition of security 2010. protocols, in: ASIA CCS '14, ACM, 2014, pp. 435-446.

  • Similar Research Results (2)
  • Metrics
    No metrics available
Share - Bookmark