Generalized probabilistic satisfiability and applications to modelling attackers with side-channel capabilities. (English) Zbl 1423.68440
Summary: We analyze a generalized probabilistic satisfiability problem (GenPSAT) which consists in deciding the satisfiability of linear inequalities involving probabilities of classical propositional formulas. GenPSAT is proved to be NP-complete and we present a polynomial reduction to Mixed-Integer Programming. Capitalizing on this translation, we implement and test a solver for the GenPSAT problem. As previously observed for many other NP-complete problems, we are able to detect a phase transition behaviour for GenPSAT. We also describe GGenPSAT, which generalizes GenPSAT by allowing Boolean combinations of linear inequalities involving probabilities of classical propositional formulas which we use to develop applications in information security. Namely, in the context of cryptographic protocols, we model classes of attackers with side-channel capabilities, and study the problem of deciding whether a formula is perfectly masked in the presence of such attackers.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 90C11 | Mixed integer programming |
| 94A60 | Cryptography |
References:
| [1] | Caleiro, C.; Casal, F.; Mordido, A., Generalized probabilistic satisfiability, (LSFA 2016. LSFA 2016, Electron. Notes Theor. Comput. Sci., vol. 332 (2016)) · Zbl 1401.68113 |
| [2] | Cook, S. A., The complexity of theorem-proving procedures, (Proceedings of 3rd ACM Symposium on Theory of Computing (1971), ACM), 151-158 · Zbl 0253.68020 |
| [3] | Biere, A.; Heule, M.; van Maaren, H., Handbook of Satisfiability, vol. 185 (2009), IOS press · Zbl 1183.68568 |
| [4] | De Moura, L.; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77 (2011) |
| [5] | Boole, G., Investigation of the Laws of Thought on Which Are Founded the Mathematical Theories of Logic and Probabilities (1853) |
| [6] | Nilsson, N. J., Probabilistic logic, Artificial Intelligence, 28, 1, 71-88 (1986) · Zbl 0589.03007 |
| [7] | Finger, M.; Bona, G., Probabilistic satisfiability: logic-based algorithms and phase transition, (IJCAI, IJCAI/AAAI (2011)), 528-533 |
| [8] | Georgakopoulos, G.; Kavvadias, D.; Papadimitriou, C. H., Probabilistic satisfiability, J. Complexity, 4, 1, 1-11 (1988) · Zbl 0647.68049 |
| [9] | Cozman, F. G.; Ianni, L. F., Probabilistic Satisfiability and Coherence Checking Through Integer Programming, 145-156 (2013) · Zbl 1390.68591 |
| [10] | Bona, G.; Cozman, F. G.; Finger, M., Generalized probabilistic satisfiability through integer programming, J. Braz. Comput. Soc., 21, 1, 1-14 (2015) |
| [11] | Finger, M.; Bona, G., Probabilistic satisfiability: algorithms with the presence and absence of a phase transition, Ann. Math. Artif. Intell., 75, 3, 351-389 (2015) · Zbl 1347.68331 |
| [12] | Mordido, A.; Caleiro, C., Probabilistic logic over equations and domain restrictions, Math. Structures Comput. Sci. (2019), in press · Zbl 1456.03045 |
| [13] | Fagin, R.; Halpern, J. Y.; Megiddo, N., A logic for reasoning about probabilities, Inform. Sci., 87, 1-2, 78-128 (1990) · Zbl 0811.03014 |
| [14] | Papadimitriou, C.; Steiglitz, K., Combinatorial Optimization: Algorithms and Complexity (1982), Dover Publications · Zbl 0503.90060 |
| [15] | Chandru, V.; Hooker, J., Optimization Methods for Logical Inference (1999), John Wiley and sons, Inc · Zbl 0997.90506 |
| [16] | Cheeseman, P.; Kanefsky, B.; Taylor, W. M., Where the really hard problems are, (IJCAI, vol. 91 (1991)), 331-340 · Zbl 0747.68064 |
| [17] | Caleiro, C.; Casal, F.; Mordido, A., Classical generalized probabilistic satisfiability, (Proceedings of IJCAI-17 (2017)), 908-914 |
| [18] | Rosenhouse, J., The Monty Hall Problem: the Remarkable Story of Math’s Most Contentious Brain Teaser (2009), Oxford University Press · Zbl 1198.00006 |
| [19] | Casal, F.; Mordido, A.; Caleiro, C., GenPSAT solver (2016), available online at |
| [20] | Chvátal, V., Linear Programming (1983), Macmillan · Zbl 0537.90067 |
| [21] | Tseitin, G. S., On the complexity of derivations in the propositional calculus, (Studies in Mathematics and Mathematical Logic Part II (1968)), 115-125 · Zbl 0197.00102 |
| [22] | Gent, I. P.; Walsh, T., The Hardest Random SAT Problems (1994), Springer |
| [23] | Gurobi Optimization, Gurobi Optimizer Reference Manual (2015) |
| [24] | Casal, F.; Mordido, A.; Caleiro, C., GGenPSAT solver (2016), available online at |
| [25] | Baltazar, P., Probabilization of Logic Systems (2010), IST - Technical University of Lisbon: IST - Technical University of Lisbon Portugal, Ph.D. thesis |
| [26] | Mordido, A., A Probabilistic Logic Over Equations and Domain Restrictions (2017), IST - Universidade de Lisboa: IST - Universidade de Lisboa Portugal, Ph.D. thesis |
| [27] | Kocher, P. C., Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems, 104-113 (1996), Springer: Springer Berlin Heidelberg · Zbl 1329.94070 |
| [28] | Kocher, P. C.; Jaffe, J.; Jun, B., Differential power analysis, (Proceedings of CRYPTO ’99 (1999), Springer-Verlag), 388-397 · Zbl 0942.94501 |
| [29] | Gandolfi, K.; Mourtel, C.; Olivier, F., Electromagnetic Analysis: Concrete Results, 251-261 (2001), Springer Berlin Heidelberg · Zbl 1006.68705 |
| [30] | Agrawal, D.; Archambeault, B.; Rao, J. R.; Rohatgi, P., The EM Side—Channel(s), 29-45 (2003), Springer Berlin Heidelberg · Zbl 1019.68535 |
| [31] | Genkin, D.; Pachmanov, L.; Pipman, I.; Tromer, E., ECDH key-extraction via low-bandwidth electromagnetic attacks on pcs, (Cryptographers’ Track at the RSA Conference (2016), Springer), 219-235 · Zbl 1334.94078 |
| [32] | Ramsay, C., Tempest Attacks Against AES (2017), White paper from Fox-IT |
| [33] | Nauerth, S.; Fürst, M.; Schmitt-Manderbach, T.; Weier, H.; Weinfurter, H., Information leakage via side channels in freespace BB84 quantum cryptography, New J. Phys., 11, 6, Article 065001 pp. (2009) |
| [34] | Boneh, D.; DeMillo, R.; Lipton, R., On the importance of checking cryptographic protocols for faults, (EUROCRYPT’97 (1997), Springer) |
| [35] | Dusart, P.; Letourneux, G.; Vivolo, O., Differential fault analysis on AES, (Applied Cryptography and Network Security (2003), Springer), 293-306 · Zbl 1131.94313 |
| [36] | Chari, S.; Jutla, C. S.; Rao, J. R.; Rohatgi, P., Towards Sound Approaches to Counteract Power-Analysis Attacks, 398-412 (1999), Springer · Zbl 0942.68045 |
| [37] | Prouff, E.; Rivain, M., Masking Against Side-Channel Attacks: A Formal Security Proof, 142-159 (2013), Springer: Springer Berlin Heidelberg · Zbl 1306.94087 |
| [38] | Eldib, H.; Wang, C.; Schaumont, P., Formal verification of software countermeasures against side-channel attacks, ACM Trans. Software Eng. Methodol., 24, 2, 11 (2014) |
| [39] | Mangard, S.; Oswald, E.; Popp, T., Power Analysis Attacks: Revealing the Secrets of Smart Cards (Advances in Information Security) (2007), Springer-Verlag New York Inc. · Zbl 1131.68449 |
| [40] | Teugels, J. L., Some representations of the multivariate Bernoulli and binomial distributions, J. Multivariate Anal., 32, 2, 256-268 (1990) · Zbl 0697.62042 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
