- -

Protocol Analysis with Time

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

  • Estadisticas de Uso

Protocol Analysis with Time

Show simple item record

Files in this item

Thumbnail
Name: Aparicio-SanchezE ...
Size: 724.0Kb
Format: PDF
Description: Versión del Autor.
Open
[Cerrado]
Name: Aparicio-Sanchez2 ...
Size: 815.2Kb
Format: PDF
Description: Versión editorial
Request a copy of the document
dc.contributor.author Aparicio-Sánchez, Damián es_ES
dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Meadows, Catherine es_ES
dc.contributor.author Meseguer, José es_ES
dc.contributor.author Sapiña-Sanchis, Julia es_ES
dc.date.accessioned 2022-01-18T08:11:15Z
dc.date.available 2022-01-18T08:11:15Z
dc.date.issued 2020-12-16 es_ES
dc.identifier.isbn 978-3-030-65276-0 es_ES
dc.identifier.issn 0302-9743 es_ES
dc.identifier.uri http://hdl.handle.net/10251/179781
dc.description.abstract [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 semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time references are represented by logical variables, and in which the properties of time are implemented as constraints on those time logical variables. These constraints are carried along the symbolic execution of the protocol. The satisfiability of these constraints can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be rejected as impossible. We demonstrate the feasibility of our approach by using the Maude-NPA protocol analyzer together with an SMT solver that is used to evaluate the satisfiability of timing constraints. We provide a sound and complete protocol transformation from our timed process algebra to the Maude-NPA syntax and semantics, and we prove its soundness and completeness. We then use the tool to analyze Mafia fraud and distance hijacking attacks on a suite of distance-bounding protocols. es_ES
dc.description.sponsorship 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 Office of Scientific Research under award number FA9550-17-1-0286, and by ONR Code 311. es_ES
dc.language Inglés es_ES
dc.publisher Springer es_ES
dc.relation.ispartof 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 es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;12578 es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Protocol Analysis with Time es_ES
dc.type Comunicación en congreso es_ES
dc.type Artículo es_ES
dc.type Capítulo de libro es_ES
dc.identifier.doi 10.1007/978-3-030-65277-7_7 es_ES
dc.relation.projectID 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/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/ONR//Code 311/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/ //FA9550-17-1-0266//Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement///PROMETEO%2F2019%2F098//DEEPTRUST/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement///APOSTD%2F2019%2F127//CONTRATO POSDOCTORAL GVA-SAPIÑA SANCHIS. PROYECTO: METODOS SIMBOLICOS AVANZADOS PARA EL ANALISIS DE SEGURIDAD DE PROTOCOLOS/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation 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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 21st International Conference on Cryptology in India (INDOCRYPT 2020) es_ES
dc.relation.conferencedate Diciembre 13-16,2020 es_ES
dc.relation.conferenceplace Online es_ES
dc.relation.publisherversion https://doi.org/10.1007/978-3-030-65277-7_7 es_ES
dc.description.upvformatpinicio 128 es_ES
dc.description.upvformatpfin 150 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.relation.pasarela S\421625 es_ES
dc.contributor.funder Office of Naval Research es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.description.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) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Clavel, M., et al.: Maude Manual (Version 3.0). Technical report, SRI International Computer Science Laboratory (2020). http://maude.cs.uiuc.edu es_ES
dc.description.references The CVC4 SMT Solver (2020). https://cvc4.github.io es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references Wolfram Mathematica (2020). https://www.wolfram.com/mathematica es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references Neumann, C., Yu, T., Hartman, S., Raeburn, K.: The Kerberos network authentication service (V5). Request Comments 4120, 1–37 (2005) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references Nigam, V., Talcott, C., Urquiza, A.A.: Symbolic timed observational equivalence. Computing Research Repository, abs/1801.04066 (2018) es_ES
dc.description.references Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1–2), 85–128 (1998) es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999) es_ES
dc.description.references Yang, F., Escobar, S., Meadows, C., Meseguer, J.: Strand spaces with choice via a process algebra semantics. Computing Research Repository, abs/1904.09946 (2019) es_ES
dc.description.references 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) es_ES
dc.description.references The Yices SMT Solver (2020). https://yices.csl.sri.com es_ES
dc.description.references The Z3 SMT Solver (2020). https://github.com/Z3Prover/z3 es_ES


This item appears in the following Collection(s)

Show simple item record