- -

Protocol Analysis with Time

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Protocol Analysis with Time

Mostrar el registro completo del ítem

Aparicio-Sánchez, D.; Escobar Román, S.; Meadows, C.; Meseguer, J.; Sapiña-Sanchis, J. (2020). Protocol Analysis with Time. Springer. 128-150. https://doi.org/10.1007/978-3-030-65277-7_7

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

Ficheros en el ítem

Thumbnail
Nombre: Aparicio-SanchezE ...
Tamaño: 724.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Aparicio-Sanchez2 ...
Tamaño: 815.2Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Protocol Analysis with Time
Autor: Aparicio-Sánchez, Damián Escobar Román, Santiago Meadows, Catherine Meseguer, José Sapiña-Sanchis, Julia
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Fecha difusión:
Resumen:
[EN] We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition ...[+]
Derechos de uso: Reserva de todos los derechos
ISBN: 978-3-030-65276-0
Fuente:
Progress in Cryptology - INDOCRYPT 2020: 21st International Conference on Cryptology in India, Bangalore, India, December 13¿16, 2020, Proceedings. Lecture Notes in Computer Science, volumen 12578. (issn: 0302-9743 )
DOI: 10.1007/978-3-030-65277-7_7
Editorial:
Springer
Versión del editor: https://doi.org/10.1007/978-3-030-65277-7_7
Título del congreso: 21st International Conference on Cryptology in India (INDOCRYPT 2020)
Lugar del congreso: Online
Fecha congreso: Diciembre 13-16,2020
Serie: Lecture Notes in Computer Science;12578
Código del Proyecto:
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/
info:eu-repo/grantAgreement/ONR//Code 311/
info:eu-repo/grantAgreement/ //FA9550-17-1-0266//Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA/
info:eu-repo/grantAgreement///PROMETEO%2F2019%2F098//DEEPTRUST/
info:eu-repo/grantAgreement///APOSTD%2F2019%2F127//CONTRATO POSDOCTORAL GVA-SAPIÑA SANCHIS. PROYECTO: METODOS SIMBOLICOS AVANZADOS PARA EL ANALISIS DE SEGURIDAD DE PROTOCOLOS/
Agradecimientos:
This paper was partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grant PROMETEO/2019/098 and APOSTD/2019/127, by the US Air Force ...[+]
Tipo: Comunicación en congreso Artículo Capítulo de libro

References

Avoine, G., et al.: A terrorist-fraud resistant and extractor-free anonymous distance-bounding protocol. In Proceedings of the Asia Conference on Computer and Communications Security (AsiaCCS 2017), pp. 800–814. ACM Press (2017)

Basin, D.A., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. ACM Trans. Inf. Syst. Securi. 14(2), 16:1–16:28 (2011)

Brands, S., Chaum, D.: Distance-bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344–359. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-48285-7_30 [+]
Avoine, G., et al.: A terrorist-fraud resistant and extractor-free anonymous distance-bounding protocol. In Proceedings of the Asia Conference on Computer and Communications Security (AsiaCCS 2017), pp. 800–814. ACM Press (2017)

Basin, D.A., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. ACM Trans. Inf. Syst. Securi. 14(2), 16:1–16:28 (2011)

Brands, S., Chaum, D.: Distance-bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344–359. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-48285-7_30

Capkun, S., Buttyán, L., Hubaux, J.-P.: SECTOR: secure tracking of node encounters in multi-hop wireless networks. In: Proceedings of the 1st ACM Workshop on Security of Ad Hoc and Sensor Networks (SASN 2003), pp. 21–32. Association for Computing Machinery (2003)

Chothia, T., de Ruiter, J., Smyth, B.: Modelling and analysis of a hierarchy of distance bounding attacks. In: Proceedings of the 27th USENIX Security Symposium (USENIX Security 2018), pp. 1563–1580. USENIX (2018)

Clavel, M., et al.: Maude Manual (Version 3.0). Technical report, SRI International Computer Science Laboratory (2020). http://maude.cs.uiuc.edu

The CVC4 SMT Solver (2020). https://cvc4.github.io

Debant, A., Delaune, S.: Symbolic verification of distance bounding protocols. In: Nielson, F., Sands, D. (eds.) POST 2019. LNCS, vol. 11426, pp. 149–174. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17138-4_7

Debant, A., Delaune, S., Wiedling, C.: A symbolic framework to analyse physical proximity in security protocols. In: Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 122, pp. 29:1–29:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Symbolic protocol analysis with disequality constraints modulo equational theories. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 238–261. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25527-9_16

Hancke, G.P., Kuhn, M.G.: An RFID distance bounding protocol. In: Proceedings of the 1st IEEE International Conference on Security and Privacy for Emerging Areas in Communications Networks (SecureComm 2005), pp. 67–73. IEEE Computer Society Press (2005)

Kim, C.H., Avoine, G., Koeune, F., Standaert, F.-X., Pereira, O.: The Swiss-Knife RFID distance bounding protocol. In: Lee, P.J., Cheon, J.H. (eds.) ICISC 2008. LNCS, vol. 5461, pp. 98–115. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00730-9_7

Wolfram Mathematica (2020). https://www.wolfram.com/mathematica

Mauw, S., Smith, Z., Toro-Pozo, J., Trujillo-Rasua, R.: Distance-bounding protocols: verification without time and location. In: Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P 2018), pp. 549–566. IEEE Computer Society Press (2018)

Meadows, C., Poovendran, R., Pavlovic, D., Chang, L.W., Syverson, P.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Poovendran, R., Roy, S., Wang, C. (eds.) Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks: Advances in Information Security, vol. 30, pp. 279–298. Springer, Boston (2007). https://doi.org/10.1007/978-0-387-46276-9_12

Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_48

Munilla, J., Peinado, A.: Distance bounding protocols for RFID enhanced by using void-challenges and analysis in noisy channels. Wirel. Commun. Mob. Comput. 8(9), 1227–1232 (2008)

Neumann, C., Yu, T., Hartman, S., Raeburn, K.: The Kerberos network authentication service (V5). Request Comments 4120, 1–37 (2005)

Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Commun. ACM 53(6), 937–977 (2006)

Nigam, V., Talcott, C., Aires Urquiza, A.: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 450–470. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45741-3_23

Nigam, V., Talcott, C., Urquiza, A.A.: Symbolic timed observational equivalence. Computing Research Repository, abs/1801.04066 (2018)

Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1–2), 85–128 (1998)

Perrig, A., Song, D., Canetti, R., Tygar, J.D., Briscoe, B.: Timed efficient stream loss-tolerant authentication (TESLA): multicast source authentication transform introduction. Request Comments 4082, 1–22 (2005)

Rasmussen, K.B., Capkun, S.: Realization of RF distance bounding. In: Proceedings of the 19th USENIX Security Symposium (USENIX Security 2010), pp. 389–402. USENIX (2010)

Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999)

Yang, F., Escobar, S., Meadows, C., Meseguer, J.: Strand spaces with choice via a process algebra semantics. Computing Research Repository, abs/1904.09946 (2019)

Yang, F., Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pp. 76–89. ACM Press (2016)

The Yices SMT Solver (2020). https://yices.csl.sri.com

The Z3 SMT Solver (2020). https://github.com/Z3Prover/z3

[-]

recommendations

 

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

Mostrar el registro completo del ítem