- -

Protocol analysis modulo combination of theories: A case study in Maude-NPA

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Protocol analysis modulo combination of theories: A case study in Maude-NPA

Show full item record

Sasse, R.; Escobar Román, S.; Meadows, C.; Meseguer, J. (2011). Protocol analysis modulo combination of theories: A case study in Maude-NPA. En Security and Trust Management. Springer Verlag (Germany). 6710:163-178. https://doi.org/10.1007/978-3-642-22444-7_11

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/35906

Files in this item

Item Metadata

Title: Protocol analysis modulo combination of theories: A case study in Maude-NPA
Author: Sasse, Ralf Escobar Román, Santiago Meadows, Catherine Meseguer, José
UPV Unit: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Issued date:
Abstract:
There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic ...[+]
Subjects: Cryptographic protocol verification , Equational unification , Exclusive or , Narrowing , Variants
Copyrigths: Reserva de todos los derechos
ISBN: 978-3-642-22443-0
Source:
Security and Trust Management. (issn: 0302-9743 )
DOI: 10.1007/978-3-642-22444-7_11
Publisher:
Springer Verlag (Germany)
Publisher version: http://link.springer.com/chapter/10.1007/978-3-642-22444-7_11
Conference name: 6th International Workshop, STM 2010
Conference place: Athens, Greece
Conference date: September 23-24, 2010
Series: Lecture Notes in Computer Science;vol. 6710
Project ID:
info:eu-repo/grantAgreement/NSF//0716638/US/CT-ISG: Attacker Models and Verification Methods for End-to-End Protocol Security/
info:eu-repo/grantAgreement/NSF//0904749/US/TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocol Analysis Tools/
info:eu-repo/grantAgreement/NSF//0831064/US/Collaborative Research: CT-M: Unification Laboratory for Cryptographic Protocol Analysis/
info:eu-repo/grantAgreement/MEC//TIN2007-68093-C02-02/ES/TECHNOLOGICS-UPV/
Thanks:
R. Sasse and J. Meseguer have been partially supported by NSF Grants CNS0716638, CNS-0831064 and CNS-0904749. S. Escobar has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN ...[+]
National Science Foundation, EEUU
Type: Capítulo de libro

References

Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)

Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 50–65. Springer, Heidelberg (1992) [+]
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)

Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 50–65. Springer, Heidelberg (1992)

Basin, D.A., Mödersheim, S., Viganò, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)

Baudet, M., Cortier, V., Delaune, S.: YAPA: A generic tool for computing intruder knowledge. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 148–163. Springer, Heidelberg (2009)

Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society, Los Alamitos (2001)

Bursuc, S., Comon-Lundh, H.: Protocol security and algebraic properties: Decision results for a bounded number of sessions. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 133–147. Springer, Heidelberg (2009)

Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: LICS, pp. 261–270. IEEE Computer Society, Los Alamitos (2003)

Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. Inf. Comput. 206(2-4), 352–377 (2008)

Chevalier, Y., Rusinowitch, M.: Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures. Theor. Comput. Sci. 411(10), 1261–1282 (2010)

Ciobâcă, Ş., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 355–370. Springer, Heidelberg (2009)

Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)

Cortier, V., Delaitre, J., Delaune, S.: Safely composing security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 352–363. Springer, Heidelberg (2007)

Cremers, C.J.F.: The scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)

Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoretical Computer Science 367(1-2), 162–202 (2006)

Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009 Tutorial Lectures. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009)

Escobar, S., Meseguer, J., Sasse, R.: Effectively checking or disproving the finite variant property. Technical Report UIUCDCS-R-2008-2960, Department of Computer Science - University of Illinois at Urbana-Champaign (April 2008)

Escobar, S., Meseguer, J., Sasse, R.: Effectively checking the finite variant property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 79–93. Springer, Heidelberg (2008)

Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electr. Notes Theor. Comput. Sci. 238(3), 103–119 (2009)

Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 52–68. Springer, Heidelberg (2010)

Fabrega, F.J.T., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security 7, 191–230 (1999)

Guo, Q., Narendran, P.: Unification and matching modulo nilpotence. In: CADE-13. LNCS, vol. 1104, pp. 261–274. Springer, Heidelberg (1996)

Harkins, D., Carrel, D.: The Internet Key Exchange (IKE), IETF RFC 2409, (November 1998)

Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361–373. Springer, Heidelberg (1983)

Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the Horn theory based approach. In: ACM Conference on Computer and Communications Security, pp. 129–138 (2008)

Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: CSF, pp. 157–171. IEEE Computer Society, Los Alamitos (2009)

Lafourcade, P., Terrade, V., Vigier, S.: Comparison of cryptographic verification tools dealing with algebraic properties. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 173–185. Springer, Heidelberg (2010)

Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

Meadows, C.: The NRL protocol analyzer: An overview. J. Log. Program. 26(2), 113–131 (1996)

Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)

Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20(1–2), 123–160 (2007)

Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)

Santiago, S., Talcott, C.L., Escobar, S., Meadows, C., Meseguer, J.: A graphical user interface for Maude-NPA. Electr. Notes Theor. Comput. Sci. 258(1), 3–20 (2009)

Schmidt-Schauß, M.: Unification in a combination of arbitrary disjoint equational theories. J. Symb. Comput. 8(1/2), 51–99 (1989)

Terese (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)

Turuani, M.: The CL-atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)

[-]

recommendations

 

This item appears in the following Collection(s)

Show full item record