- -

Analysis of the IBM CCA Security API Protocols in Maude-NPA

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Analysis of the IBM CCA Security API Protocols in Maude-NPA

Mostrar el registro completo del ítem

González Burgueño, A.; Santiago Pinazo, S.; Escobar Román, S.; Meadows, C.; Meseguer, J. (2014). Analysis of the IBM CCA Security API Protocols in Maude-NPA. En Security Standardisation Research. Springer International Publishing. 111-130. https://doi.org/10.1007/978-3-319-14054-4_8

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

Ficheros en el ítem

Thumbnail
Nombre: SSR2014-cameraRea ...
Tamaño: 502.1Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: chp%3A10.1007%2F9 ...
Tamaño: 322.1Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Analysis of the IBM CCA Security API Protocols in Maude-NPA
Autor: González Burgueño, Antonio Santiago Pinazo, Sonia Escobar Román, Santiago Meadows, Catherine Meseguer, Jose
Editor: Springer Lecture Notes in Computer Science, Vol. 8893
Entidad UPV: Universitat Politècnica de València. Grupo de Extensiones de la Programación Lógica (ELP)
Fecha difusión:
Resumen:
Standards for cryptographic protocols have long been attractive candidates for formal verification. It is important that such standards be correct, and cryptographic protocols are tricky to design and subject to ...[+]
Palabras clave: IBM 4758 common cryptographic architecture , Security Application Programming Interfaces (security APIs) , Symbolic cryptographic protocol analysis , Automatic reasoning modulo XOR theory
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-319-14054-4 978-3-319-14053-7
Fuente:
Security Standardisation Research. (issn: 0302-9743 )
DOI: 10.1007/978-3-319-14054-4_8
Editorial:
Springer International Publishing
Versión del editor: https://doi.org/10.1007/978-3-319-14054-4_8
Título del congreso: 1st International Conference on Research in Security Standardisation (SSR 2014)
Lugar del congreso: London, UK
Fecha congreso: 2014-12-16
Serie: Lecture Notes in Computer Science;8893
Código del Proyecto:
info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
info:eu-repo/grantAgreement/NSF//1319109/US/TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude/
info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/
Agradecimientos:
Antonio González-Burgueño, Sonia Santiago and Santiago Escobar have been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana ...[+]
Tipo: Capítulo de libro Comunicación en congreso

References

Abadi, M., Blanchet, B., Fournet, C.: Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. 10(3) (2007)

Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW 2014), Cape Breton, Nova Scotia, Canada, June 2001, pp. 82–96. IEEE Computer Society (2014)

Bond, M.: Attacks on cryptoprocessor transaction sets. In: Koç, Ç.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol. 2162, pp. 220–234. Springer, Heidelberg (2001) [+]
Abadi, M., Blanchet, B., Fournet, C.: Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. 10(3) (2007)

Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW 2014), Cape Breton, Nova Scotia, Canada, June 2001, pp. 82–96. IEEE Computer Society (2014)

Bond, M.: Attacks on cryptoprocessor transaction sets. In: Koç, Ç.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol. 2162, pp. 220–234. Springer, Heidelberg (2001)

Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A formal analysis of some properties of kerberos 5 using msr. In: CSFW, pp. 175–1790. IEEE Computer Society (2002)

Cachin, C., Chandran, N.: A secure cryptographic token interface. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, pp. 141–153 (2009)

Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: 18th Annual IEEE Symposium on Logic in Computer Science, LICS 2003 (2003)

Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive-or. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 271–280 (2003)

Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148–164. Springer, Heidelberg (2003)

Cortier, V., Keighren, G., Steel, G.: Automatic analysis of the aecurity of XOR-based key management schemes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 538–552. Springer, Heidelberg (2007)

Cortier, V., Steel, G.: A generic security API for symmetric key management on cryptographic devices. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 605–620. Springer, Heidelberg (2009)

Erbatur, S., et al.: Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73–90. Springer, Heidelberg (2012)

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. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)

Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Sequential Protocol Composition in Maude-NPA. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 303–318. Springer, Heidelberg (2010)

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

González-Burgueño, A.: Protocol Analysis Modulo Exclusive-Or Theories: A Case study in Maude-NPA. Master’s thesis, Universitat Politècnica de València (March 2014), https://angonbur.webs.upv.es/Previous_work/Master_Thesis.pdf

IBM. Comment on Mike’s Bond paper A Chosen Key Difference Attack on Control Vectors (2001), http://www.cl.cam.ac.uk/~mkb23/research/CVDif-Response.pdf

IBM. CCA basic services reference and guide: CCA basic services reference and guide for the IBM 4758 PCI and IBM 4764 (2001), http://www-03.ibm.com/security/cryptocards/pdfs/bs327.pdf.2008

Keighren, G.: Model Checking IBM’s Common Cryptographic Architecture API. Technical Report 862, University of Edinburgh (October 2006)

Kemmerer, R.A.: Using formal verification techniques to analyze encryption protocols. In: IEEE Symposium on Security and Privacy, pp. 134–139. IEEE Computer Society (1987)

Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the horn theory based approach. J. Autom. Reasoning 46(3-4), 325–352 (2011)

Linn, J.: Generic security service application program interface version 2, update 1. IETF RFC 2743 (2000), https://datatracker.ietf.org/doc/rfc2743

Longley, D., Rigby, S.: An automatic search for security flaws in key management schemes. Computers & Security 11(1), 75–89 (1992)

Meadows, C.: Applying formal methods to the analysis of a key management protocol. Journal of Computer Security 1(1) (1992)

Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)

Meadows, C., Cervesato, I., Syverson, P.: Specification and Analysis of the Group Domain of Interpretation Protocol using NPATRL and the NRL Protocol Analyzer. Journal of Computer Security 12(6), 893–932 (2004)

Meadows, C.: Analysis of the internet key exchange protocol using the nrl protocol analyzer. In: IEEE Symposium on Security and Privacy, pp. 216–231. IEEE Computer Society (1999)

Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic snalysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)

Mukhamedov, A., Gordon, A.D., Ryan, M.: Towards a verified reference implementation of a trusted platform module. In: Christianson, B., Malcolm, J.A., Matyáš, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 69–81. Springer, Heidelberg (2013)

National Institute of Standards and Technology. FIPS PUB 46-3: Data Encryption Standard (DES), supersedes FIPS 46-2 (October 1999)

Nieuwenhuis, R. (ed.): CADE 2005. LNCS (LNAI), vol. 3632. Springer, Heidelberg (2005)

Steel, G.: Deduction with xor constraints in security api modelling. In: Nieuwenhuis (ed.) [30], pp. 322–336

Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis (ed.) [30], pp. 337–352

[-]

recommendations

 

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro completo del ítem