Geodesic
Even simple processes of $\pi$-calculus are hard for analysis
Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 589-606.

Voir la notice de l'article provenant de la source Math-Net.Ru

Mathematical models of distributed computations, based on the calculus of mobile processes ($\pi$-calculus) are widely used for checking the information security properties of cryptographic protocols. Since $\pi$-calculus is Turing-complete, this problem is undecidable in general case. Therefore, the study is carried out only for some special classes of $\pi$-calculus processes with restricted computational capabilities, for example, for non-recursive processes, in which all runs have a bounded length, for processes with a bounded number of parallel components, etc. However, even in these cases, the proposed checking procedures are time consuming. We assume that this is due to the very nature of the $\pi$ -calculus processes. The goal of this paper is to show that even for the weakest model of passive adversary and for relatively simple protocols that use only the basic $\pi$-calculus operations, the task of checking the information security properties of these protocols is co-NP-complete.
Mots-clés : $\pi$-calculus, protocol
Keywords: security, passive adversary, verification, complexity, NP-completeness. 
@article{MAIS_2018_25_6_a0,
     author = {M. M. Abbas and V. A. Zakharov},
     title = {Even simple processes of $\pi$-calculus are hard for analysis},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {589--606},
     publisher = {mathdoc},
     volume = {25},
     number = {6},
     year = {2018},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a0/}
}
TY  - JOUR
AU  - M. M. Abbas
AU  - V. A. Zakharov
TI  - Even simple processes of $\pi$-calculus are hard for analysis
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2018
SP  - 589
EP  - 606
VL  - 25
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a0/
LA  - ru
ID  - MAIS_2018_25_6_a0
ER  - 
%0 Journal Article
%A M. M. Abbas
%A V. A. Zakharov
%T Even simple processes of $\pi$-calculus are hard for analysis
%J Modelirovanie i analiz informacionnyh sistem
%D 2018
%P 589-606
%V 25
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a0/
%G ru
%F MAIS_2018_25_6_a0
M. M. Abbas; V. A. Zakharov. Even simple processes of $\pi$-calculus are hard for analysis. Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 589-606. http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a0/

[1] Abadi M., Gordon A. D., “A Calculus for Cryptographic Protocols: The Spi Calculus”, Information and Computation, 148:1 (1999), 1–70 | DOI | MR | Zbl

[2] Abadi M., Fournet C., “Mobile Values, New Names, and Secure Communication”, Proceedings of the 28-th ACM Symposium on Principles of Programming Languages, 2001, 104–115 | MR | Zbl

[3] Amadio M. R., Lugiez D., “On the Reachability Problem for Cryptographic Protocols”, Proceedings of the 11-th International Conference on Concurrency Theory, 2000, 380–394 | MR | Zbl

[4] Amadio M. R., Lugiez D., Vanackere V., “On the symbolic reduction of processes with cryptographic functions”, Theoretical Computer Science, 290:1 (2003), 695–740 | DOI | MR | Zbl

[5] Arapinis M., Liu J., Ritter E., Ryan M., “Stateful Applied Pi Calculus”, Proceedings of the Principles of Security and Trust–Third International Conference, 2014, 22–41 | DOI

[6] Blanchet B., Smith B., “Automated reasoning for equivalences in the applied pi calculus with barriers”, Proceedings of the 29-th IEEE Computer Security Foundations Symposium, 2014, 310–324

[7] Bodei C., Degano P., Nielson F., Nielson H. R., “Static Analysis for the pi-Calculus with Applications to Security”, Information and Computation, 168:1 (2001), 68–92 | DOI | MR | Zbl

[8] Borgstrom J., Nestmann U., “On bisimulations for the spi calculus”, Mathematical Structures in Computer Science, 15:3 (2005), 487–552 | DOI | MR | Zbl

[9] Bruni A., Modersheim S., Nielson F., Nielson H. R., “Set-Pi: Set Membership Pi-Calculus”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 185–198

[10] Chadha R., Cheval V., Ciobaca S., Kremer S., “Automated Verification of Equivalence Properties of Cryptographic Protocols”, ACM Transactions on Computational Logic, 17:4 (2016), 1–32 | DOI | MR

[11] Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents”, Proceedings of the 23-rd Annual Conference on the Foundations of Software Technology and Theoretical Computer Science, 2003, 124–135 | MR | Zbl

[12] Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “An NP decision procedure for protocol insecurity with XOR”, Theoretical Computer Science, 338:1–3 (2005), 247–274 | DOI | MR | Zbl

[13] Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Deciding the security of protocols with commuting public key encryption”, Electronic Notes in Theoretical Computer Science, 125:1 (2005), 55–66 | DOI | MR | Zbl

[14] Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption”, ACM Transactions on Computational Logic, 9:4 (2008), 1–52 | DOI | MR

[15] Chretien R., Cortier V., Delaune S., “Decidability of trace equivalence for protocols with nonces”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 170–184

[16] Cortier V., Delaune S., “A method for proving observational equivalence”, Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, 2009, 266–276 | DOI

[17] Curti M., Degano P., Priami C., Balardi C. T., “Modelling biochemical pathways through enhanced pi-calculus”, Theoretical Computer Science, 325:1 (2004), 111–140 | DOI | MR | Zbl

[18] Delaune S., Ryan M., Smyth B., “Automatic verification of privacy properties in the applied pi calculus”, Trust Management II, IFIP International Federation for Information Processing, 263, Springer, Boston, 2008, 263–278 | DOI

[19] Dolev D., Yao A., “On the security of public key protocols”, IEEE Transactoions on Information Theory, 29:2 (1983), 198–208 | DOI | MR | Zbl

[20] Durante L., Sisto R., Valenzano A., “Automatic Testing Equivalence Verification of Spi Calculus Specifications”, ACM Transactions on Software Engineering and Methodology, 12:2 (2003), 222–284 | DOI | MR

[21] Durgin N. A., Lincoln P., Mitchell J. C., “Multiset rewriting and the complexity of bounded security protocols”, Journal of Computer Security, 12:2 (2004), 247–311 | DOI

[22] Godskesen J. C., “Formal Verification of the ARAN Protocol Using the Applied Pi-calculus”, Proceedings of the Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, 2006, 99–113

[23] Huima A., “Efficient infinite state analysis of security protocols”, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999

[24] Liang Z., Verma R. M., “Correcting and Improving the NP Proof for Cryptographic Protocol Insecurity”, Proceedings of the 5-th International Conference on Information Systems Security, 2009, 101–116 | DOI

[25] Milner R., Parrow J., Walker D., “A calculus of mobile processes. I; II”, Information and Computation, 100:1 (1992), 1–40 ; 41–77 | DOI | MR | Zbl | MR | Zbl

[26] Milner R., “Functions as Processes”, Mathematical Structures in Computer Science, 2 (1992), 119–141 | DOI | MR | Zbl

[27] Milner R., Communicating and mobile systems — the Pi-calculus, MIT Press, 1999 | MR

[28] Regev A., “Representation and Simulation of Biochemical Processes Using the pi-Calculus Process Algebra”, Proceedings of the 6-th Pacific Symposium on Biocomputing, 2001, 459–470

[29] Rusinowitch M., Turuani M., “Protocol Insecurity with Finite Number of Sessions is NP-complete”, Theoretical Computer Science, 299:1–3 (2003), 451–475 | DOI | MR | Zbl

[30] Smith H., Fingar P., Business Process Management: The Third Wave, Meghan-Kiffer Press, Tampa, 2003

[31] Tiplea F. L., Enea C., Birjoveanu C. V., “Decidability and complexity results for security protocols”, Verification of Infinite-State Systems with Applications to Security, IOS Press, Amsterdam, 2006, 185–211 | MR

[32] Tiu A., Dawson J., “Automating Open Bisimulation Checking for the Spi Calculus”, Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010, 307–321 | DOI

[33] Walker D., “Objects in the $\pi$-calculus”, Information and Computation, 116:4 (1995), 253–271 | DOI | MR | Zbl