Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Bugliesi, Michele; Calzavara, Stefano; Mödersheim, Sebastian; Modesti, Paolo (2016)
Publisher: Elsevier
Languages: English
Types: Article
Subjects: 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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [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.
    • [11] P. Modesti, Efficient Java code generation of security protocols specified in An- [24] T. Gibson-Robinson, Analysing layered seB/AnBx, in: STM'14, 2014, pp. 204-208. curity protocols, Ph.D. thesis, University of Oxford (2013).
    • [12] P. Modesti, Anbx: Automatic generation and verification of security protocols imple- [25] C. Sprenger, D. Basin, Developing security mentations, in: FPS'15, Vol. 9482 of LNCS, protocols by refinement, in: CCS'10, ACM Springer, 2016. Press, 2010.
    • [13] M. Abadi, C. Fournet, G. Gonthier, Authentication primitives and their compilation, in: POPL'00, ACM New York, NY, USA, 2000, pp. 302-315.
    • [14] P. Adao, C. Fournet, Cryptographically sound implementations for communicating processes, in: ICALP'06, Vol. 4052, Springer, 2006, pp. 83-94.
    • [15] R. Corin, P.-M. D´enielou, C. Fournet, K. Bhargavan, J. J. Leifer, Secure implementations of typed session abstractions, in: CSF'07, IEEE, 2007, pp. 170-186.
    • [16] K. Bhargavan, R. Corin, P.-M. D´enielou, C. Fournet, J. J. Leifer, Cryptographic protocol synthesis and verification for multiparty sessions, in: CSF'09, 2009.
    • [17] C. Dilloway, G. Lowe, On the specification of secure channels, in: WITS'07, 2007.
    • [18] M. Bugliesi, R. Focardi, Language based secure communication, in: CSF'08, 2008, pp. 3-16.
    • [19] A. Armando, R. Carbone, L. Compagna, LTL model checking for security protocols, in: CSF'07, 2007, pp. 385-396.
    • [26] C. Sprenger, D. Basin, Refining key establishment, in: CSF'12, Vol. 0, IEEE Computer Society, Los Alamitos, CA, USA, 2012, pp. 230-246.
    • [27] D. Basin, S. Mo¨dersheim, L. Vigan`o, OFMC: A symbolic model checker for security protocols, International Journal of Information Security 4 (3) (2005) 181-208.
    • [28] M. Bellare, J. Garay, R. Hauser, A. Herzberg, H. Krawczyk, M. Steiner, G. Tsudik, M. Waidner, iKP a family of secure electronic payment protocols, in: 1st USENIX Workshop on Electronic Commerce, 1995.
    • [29] M. Bellare, J. Garay, R. Hauser, A. Herzberg, H. Krawczyk, M. Steiner, G. Tsudik, E. Van Herreweghen, M. Waidner, Design, implementation, and deployment of the iKP secure electronic payment system, IEEE Journal on Selected Areas in Communications 18 (4) (2000) 611-627.
    • [30] G. Bella, F. Massacci, L. Paulson, Verifying the SET registration protocols, IEEE Journal on Selected Areas in Communications 21 (1) (2003) 77-87.
    • [31] G. Bella, F. Massacci, L. Paulson, An [43] D. O'Mahony, M. Peirce, H. Tewari, Elecoverview of the verification of SET, Interna- tronic payment systems for e-commerce, tional Journal of Information Security 4 (1) Artech House Publishers, 2001. (2005) 17-28.
    • [32] G. Bella, F. Massacci, L. Paulson, Verifying the SET purchase protocols, Journal of Automated Reasoning 36 (1) (2006) 5-37.
    • [44] K. Ogata, K. Futatsugi, Formal analysis of the iKP electronic payment protocols, in: ISSS'02, LNCS, Springer, 2003, pp. 441- 460.
    • [33] M. Bugliesi, P. Modesti, AnBx - Secu- [45] S. Brlek, S. Hamadou, J. Mullins, A flaw in rity protocols design and verification, in: the electronic commerce protocol SET, InARSPA-WITS'10, Springer-Verlag, 2010, formation Processing Letters 97 (3) (2006) pp. 164-184. 104-108.
    • [34] G. Lowe, A hierarchy of authentication [46] J. K. Millen, V. Shmatikov, Constraint specifications, in: CSFW'97, IEEE Com- solving for bounded-process cryptographic puter Society Press, 1997, pp. 31-43. protocol analysis, in: CCS'01, ACM Press, 2001, pp. 166-175.
    • [35] AVISPA, Deliverable 2.3: The termediate Format, available www.avispa-project.org (2003).
    • at [47] M. Rusinowitch, M. Turuani, Protocol insecurity with a finite number of sessions, composed keys is NP-complete, Theor. Comput. Sci. 1-3 (299) (2003) 451-475.
    • [37] J. Heather, G. Lowe, S. Schneider, How to prevent type flaw attacks on security protocols, Journal of Computer Security 11 (2) (2003) 217-244.
    • [36] S. Mo¨dersheim, Algebraic properties in Alice and Bob notation (extended version), Tech. Rep. RZ3709, IBM Zurich Re- [48] D. Basin, S. Mo¨dersheim, L. Vigan`o, search Lab, domino.research.ibm.com/ OFMC: A symbolic model checker for seculibrary/cyberdig.nsf (2008). rity protocols, International Journal of Information Security 4 (3) (2005) 181-208.
    • Appendix A. Proof of Theorem 2
    • [38] M. Arapinis, M. Duflot, Bounding messages The idea behind the proof is to abuse a popfor free in security protocols, in: V. Arvind, ular verification technique as a proof argument, S. Prasad (Eds.), FSTTCS 2007, Vol. 4855 namely the symbolic constraint-based approach of LNCS, Springer, New Delhi, India, 2007, that we call “the lazy intruder” [46, 47, 48, 39]. pp. 376-387. The intuition behind the lazy intruder is as follows. Every trace can be seen as an instance
    • [39] S. Mo¨dersheim, Deciding security for a of a symbolic trace, i.e., a sequence of transition fragment of ASLan, in: ESORICS'12, 2012, rule applications where we delay the unification pp. 127-144. of left-hand side ik(m) facts and leave variables in there uninstantiated. Instead, we keep a con-
    • [40] B. Blanchet, An efficient cryptographic straint M ⊢ m, where M is the set of messages protocol verifier based on Prolog rules, in: the intruder knows at that state. Such a conCSFW'14, IEEE Computer Society, Cape straint expresses that the intruder must be able Breton, Nova Scotia, Canada, 2001, pp. 82- to generate the message m from knowledge M. 96. Thus, these constraints before reduction contain
    • [41] A. Armando, L. Compagna, SAT-based only messages m, or instances thereof, for which Model-Checking for Security Protocols ik(m) occurs in the IF specification of the proAnalysis, International Journal of Informa- tocol P (in the transition rules of the honest tion Security 6 (1) (2007) 3-32. agents). It can be shown that, if there is an attack trace, then there is a corresponding sym-
    • [42] E. Van Herreweghen, Non-repudiation in bolic trace with satisfiable intruder constraints, SET: Open issues, in: FC'01, LNCS, hence in the proof we can focus without loss of Springer, 2001, pp. 140-156. generality on such symbolic traces.
  • No related research data.
  • Discovered through pilot similarity algorithms. Send us your feedback.

Share - Bookmark

Funded by projects


Cite this article