- -

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

Show full item record

Erbatur, S.; Escobar Román, S.; Kapur, D.; Liu, Z.; Lynch, CA.; Meadows, C.; Meseguer, J.... (2013). Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. En Automated Deduction – CADE-24. Springer. 231-248. doi:10.1007/978-3-642-38574-2_16

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

Files in this item

Item Metadata

Title: Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
Author:
UPV Unit: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica
Issued date:
Abstract:
We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition ...[+]
Copyrigths: Reserva de todos los derechos
ISBN: 978-3-642-38573-5
Source:
Automated Deduction – CADE-24. (issn: 0302-9743 )
DOI: 10.1007/978-3-642-38574-2_16
Publisher:
Springer
Publisher version: http://link.springer.com/chapter/10.1007/978-3-642-38574-2_16
Conference name: 24th International Conference on Automated Deduction (CADE - 24)
Conference place: Lake Placid, New York, USA
Conference date: June 9-14, 2013
Series: Lecture Notes in Computer Science;7898
Description: The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-38574-2_16
Type: Capítulo de libro Comunicación en congreso

References

IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999)

Basin, D., 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)

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001) [+]
IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999)

Basin, D., 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)

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

Bürckert, H.-J., Herold, A., Schmidt-Schauß, M.: On equational theories, unification, and (un)decidability. Journal of Symbolic Computation 8(1/2), 3–49 (1989)

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)

Durán, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)

Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: 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)

Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Sasse, R.: Asymmetric unification: A new unification paradigm for cryptographic protocol analysis. In: UNIF 2011 (2011), https://sites.google.com/a/cs.uni.wroc.pl/unif-2011/program

Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7-8), 898–928 (2012)

Harju, T., Karhumäki, J., Krob, D.: Remarks on generalized post correspondence problem. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 39–48. Springer, Heidelberg (1996)

Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation - international edition, 2nd edn. Addison-Wesley (2003)

Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)

Liu, Z., Lynch, C.: Efficient general unification for XOR with homomorphism. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 407–421. Springer, Heidelberg (2011)

Liu, Z.: Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis. PhD thesis, Clarkson University (2012), http://people.clarkson.edu/~clynch/papers/Dissertation_of_Zhiqiang_Liu.pdf

Lowe, G., Roscoe, A.W.R.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering 23, 659–669 (1997)

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

Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proc. CSF 2012, pp. 78–94. IEEE (2012)

Tatebayashi, M., Matsuzaki, N., Newman Jr., D.B.: Key distribution protocol for digital mobile communication systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324–334. Springer, Heidelberg (1990)

TeReSe, editor. Term Rewriting Systems. Cambridge University Press (2003)

Viry, P.: Equational rules for rewriting logic. Theor. Comp. Sci. 285(2), 487–517 (2002)

[-]

This item appears in the following Collection(s)

Show full item record