Publications

• A. Armando, A. Merlo, M. Migliardi, L. Verderame. Breaking and fixing the Android Launching Flow. In Computers & Security. In press.
• A. Armando, R. Carbone, L. Zanetti. Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols. In the Proceedings of the 7th International Conference on Network and System Security (NSS 2013) , Madrid, Spain, June 3 - 4, 2013.
• A. Armando, R. Carbone, A. Merlo. Formal Analysis of a Privacy-Preserving Billing Protocol. In the Proceedings of the 1st EIT ICT Labs Workshop on Smart Grid Security (SmartGridSec 2012), Berlin, Germany, December 3, 2012.
• A. Armando, G. Costa, A. Merlo, and L. Verderame. Bring Your Own Device, Securely. In the Proceedings of the 28th ACM Symposium on Applied Computing, Computer Security track (SEC@SAC 2013), Coimbra, Portugal, March 18 - 22, 2013.
• A. Armando, R. Carbone, L. Compagna, J. Cuéllar, G. Pellegrino, A. Sorniotti. An authentication flaw in browser-based Single Sign-On protocols: Impact and remediations. In Computers & Security, Volume 33, pages 41-58, 2013.
• A. Armando, G. Costa, A. Merlo, and L. Verderame. Securing the ``Bring Your Own Device'' Policy. In the Journal of Internet Services and Information Security, ISSN: 2182-2069, Vol.2 No. 3, November 2012, pp.3-18.
• A. Armando and S. Ranise. Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving. In the Journal of Computer Security, Volume 20, Number 4, pages 309-352, 2012.
• S. Ranise and A. Armando. On the Automated Analysis of Safety in Usage Control: A New Decidability Result. In the Proceedings of the 6th International Conference on Network and System Security, Wu Yi Shan, Fujian, China, November 21-23, 2012.
• A. Armando, G. Costa, A. Merlo. Formal Modeling and Verification of the Android Security Framework. In the Proceedings of the 7th International Symposium on Trustworthy Global Computing (TGC 2012), Newcastle upon Tyne, UK, 7-8 September 2012.
• S. Ranise, A. T. Truong. A. Armando. Boosting Model Checking to Analyse Large ARBAC Policies. In the Proceedings of the 8th International Workshop on Security and Trust Management (STM 2012), Pisa, Italy - September 13-14, 2012.
• A. Armando, A. Contento, D. Costa, M. Maratea. Minimum Disclosure as Boolean Optimization: New Results. In the Proceedings of the 19th RCRA International Workshop on "Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion" (RCRA 2012), Rome, Italy, June 14-16, 2012.
• A. Armando, G. Pellegrino, R. Carbone, A. Merlo, D. Balzarotti. From Model-checking to Automated Testing of Security Protocols: Bridging the Gap. In the Proceedings of the 6th International Conference on Tests & Proofs, Prague, Czech Republic, May 31 - June 1, 2012.
• A. Armando, A. Merlo, M. Migliardi, and L. Verderame. Would You Mind Forking This Process? A Denial of Service attack on Android (and Some Countermeasures). In the Proceedings of the 27th IFIP International Information Security and Privacy Conference (SEC 2012), Heraklion, Crete, Greece, June 4-6, 2012.
• A. Armando, W. Arsac, T. Avanesov, M. Barletta, A. Calvi, A. Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cuéllar, G. Erzse, S. Frau, M. Minea, S. Mödersheim, D. von Oheimb, G. Pellegrino, S. E. Ponta, M. Rocchetto, M. Rusinowitch, M. Torabi Dashti, M. Turuani, and L. Viganò. The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In the Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Talling, Estonia, March 24 - April 1, 2012.
• A. Armando, S. Ranise, F. Turkmen, and B. Crispo. Efficient Run-time Solving of RBAC User Authorization Queries: Pushing the Envelope. In the Proceedings of the 2nd ACM Conference on Data and Application Security and Privacy (CODASPY'12), San Antonio, TX (USA), February 7-9, 2012.
• A. Armando, R. Carbone, L. Compagna, G. Pellegrino. Automatic Security Analysis of SAML-based Single Sign-On Protocols. In ``Digital Identity and Access Management: Technologies and Frameworks'', R. Sharman, S. Das Smith and M. Gupta, editors, IGI Global, 2012.
• A. Armando, E. Giunchiglia, M. Maratea and S. E. Ponta. An Action-based Approach to the Formal Specification and Automatic Analysis of Business Processes under Authorization Constraints. In the Journal of Computer and System Sciences vol. 1, pages 119-141, 2012.
• A. Armando, R. Carbone, and S. Ranise. Automated Analysis of Semantic-Aware Access Control Policies: a Logic-Based Approach. In the Proceedings of the IEEE Workshop on Semantic Computing for Security and Privacy, San Francisco (USA), September 21, 2011.
• A. Armando and S. Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies. In the Proceedings of the 7th International Workshop on Security and Trust Management, Copenhagen (Denmark), July 27-28, 2011.
• F. Alberti, A. Armando, and S. Ranise. ASASP: Automated Symbolic Analysis of Administrative Policies. In Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), Wroclaw (Poland), July 31-August 5, 2011.
• A. Armando, R. Carbone, L. Compagna, J. Cuéllar, G. Pellegrino, A. Sorniotti. From Multiple Credentials to Browser-based Single Sign-On: Are We More Secure? In the Proceedings of the 26th IFIP TC-11 International Information Security Conference (SEC 2011), Luzern (Switzerland), June 7-9, 2011.
• F. Alberti, A. Armando and S. Ranise. Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-Policies. In Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS'11), Hong Kong, March 22-24, 2011.
• A. Armando and S. Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proceedings of 6th International Workshop on Security and Trust Management (STM'10), Athens, September 23-24, 2010.
• A. Merlo and A. Armando. Cooperative Access Control for the Grid. Proceedings of the 6th International Conference on Information Assurance and Security (IAS 2010), Atlanta, GA, USA, August 23-24, 2010.
• A. Armando and S. E. Ponta. Model Checking of Security-sensitive Business Processes. Proceedings of the 6th International Workshop on Formal Aspects in Security and Trust (FAST2009), Eindhoven, the Netherlands, November 5-6, 2009.
• A. Armando. Building SMT-based Software Model Checkers: an Experience Report. (Invited Paper) In the proceeding of the 7th International Symposium on Frontiers of Combining Systems (FroCoS'09), Trento, Italy, September 16-18, 2009.
• A. Armando, R. Carbone and L. Compagna. LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics, special issue on Logic and Information Security, vol. 19/4, pp. 403-429, 2009.
• A. Armando, E. Giunchiglia and S. E. Ponta. Formal Specification and Automatic Analysis of Business Processes under Authorization Constraints: an Action-based Approach. Proceedings of the 6th International Conference on Trust, Privacy & Security in Digital Business (TrustBus'09), August 31 - September 4, 2009, Linz, Austria.
• A. Armando, R. Carbone, L. Compagna, J. Cuéllar and L. Tobarra. Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In the proceeding of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), October 27th, 2008, Hilton Alexandria Mark Center, Virginia, USA.
  • See the following page for more information.
• A. Armando, J. Mantovani and L. Platania. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers. International Journal on Software Tools for Technology Transfer (STTT), volume 11, issue 1, pp. 69-83, 2009.
• A. Armando, M. Benerecetti, D. Carotenuto, J. Mantovani and P. Spica. The Eureka Tool for Software Model Checking. In the proceedings of the 22nd IEEE/ACM ASE Conference, November 5-9, 2007, Atlanta, Georgia, USA.
• A. Armando and L. Compagna. SAT-based Model Checking for Security Protocols Analysis. International Journal of Information Security, vol. 7, no. 1. January 2008.
• A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic (TOCL), vol. 10, no. 1, pp. 1-51, 2009.
• A. Armando, R. Carbone and L. Compagna. LTL Model Checking for Security Protocols. In the proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF20), July 6-8, 2007, Venice, Italy.
• A. Armando, M. Benerecetti and J. Mantovani. Abstraction Refinement of Linear Programs with Arrays. In the Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), March 24-April 1, 2007, Braga, Portugal, LNCS 4424, pp. 373-388.
• A. Armando, J. Mantovani and L. Platania. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers. In the Proceedings of the 13th International SPIN Workshop on Model Checking of Software (SPIN'06), March 30-April 1, 2006, Vienna, Austria. LNCS 3925, Pp. 146-162.
• A. Armando, D. Basin, J. Cuéllar, M. Rusinowitch L. Viganò. AVISPA: Automated Validation of Internet Security Protocols and Applications, ERCIM News, no. 64, page 66-67, January 2006.
• A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In the Proceedings of 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005), Vienna Austria, September 19-21, 2005. Pp. 65-80, Springer Verlag.
• A. Armando, M. Benerecetti, J. Mantovani. Model Checking Linear Programs with Arrays. In the Proceedings of the 3rd Workshop on Software Model Checking (SoftMC'05), July 11, 2005 Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science vol. 144/3, pp. 79-94, 2006.
• A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuéllar, P. Hankes Drielsma, P.C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, L. Vigneron. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In the Proceedings of the 17th International Conference on Computer-Aided Verification (CAV'05), Edinburgh, Scotland, July 6-10, 2005.
• A. Armando, C. Castellini, E. Giunchiglia, M. Maratea. The SAT-based Approach to Separation Logic. Journal of Automated Reasoning. Vol. 35. Nos. 1-3, pp. 237-263, 2005.
• A. Armando, L. Compagna, S. Ranise. Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of his 60th Birthday. D. Hutter and W. Stephan (Eds.). Lecture Notes in Computer Science, Volume 2605, Jan 2005, Pp. 30-45, Springer Verlag.
• A. Armando, C. Castellini, E. Giunchiglia, F. Giunchiglia, A. Tacchella. SAT-Based Decision Procedures for Automated Reasoning: a Unifying Perspective. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of his 60th Birthday. D. Hutter and W. Stephan (Eds.). Lecture Notes in Computer Science, Volume 2605, Jan 2005, Pp. 46-58, Springer Verlag.
• A. Armando, C. Ballarin. A Reconstruction and Extension of Maple's Assume Facility via Constraint Contextual Rewriting. Journal of Symbolic Computation, vol. 39/5, pp. 503-521, 2005. ISSN: 0747-7171.
• A. Armando, C. Castellini, and J. Mantovani. Software Model Checking using Linear Constraints. In the Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04), Nov 8-12, 2004, Seattle, USA.
• A. Armando and L. Compagna. SATMC: a SAT-based Model Checker for Security Protocols. In proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), September 27-30, 2004, Lisbon, Portugal.
• A. Armando, L. Compagna, and Y. Lierler. Automatic Compilation of Protocol Insecurity Problems into Logic Programming. In proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), September 27-30, 2004, Lisbon, Portugal.
• A. Armando, C. Castellini, E. Giunchiglia, M. Idini, and M. Maratea. TSAT++: an Open Platform for Satisfiability Modulo Theories. In the Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'04), July 05, 2004, Cork, Ireland. In Electronic Notes in Theoretical Computer Science vol. 125 pp. 25-36.
• A. Armando and L. Compagna. An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols. In the Electronic Notes in Theoretical Computer Science Volume 125, Issue 1, 3 March 2005, Pages 91 108, special issue on Automated Reasoning for Security Protocol Analysis (ARSPA).
• A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea. A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints. In the Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04). May 10-13 2004, Vancouver, BC, Canada.
• A. Armando, L. Compagna and P. Ganty. SAT-based Model-Checking of Security Protocols using Planning Graph Analysis. In the proceedings of the 12th International FME Symposium (FME 2003), September 8-14 2003, Pisa, Italy. LNCS 2885. Copyright © Springer-Verlag.
• A. Armando and L. Compagna. Abstraction-driven SAT-based Analysis of Security Protocols. In the proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), May 5-8, 2003, S.Margherita Ligure, Italy. LNCS 2919. Copyright © Springer-Verlag.
• A. Armando and S. Ranise. Constraint Contextual Rewriting. Journal of Symbolic Computation, Volume 36, Issues 1-2, pp. 193-216, 2003. Special Issue on FTP 2000, International Workshop on First-Order Theorem Proving. Peter Baumgartner and Hantao Zhang, Editors.
• A. Armando, S. Ranise, M. Rusinowitch. The Rewriting Approach to Satisfiability Procedures. Information and Computation 183 (2003) pp. 140-164.
• A. Armando and L. Compagna. Automatic SAT-compilation of Protocol Insecurity Problems via Reduction to Planning. In the Proceedings of the Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002), November 11-14, 2002, Houston, Texas, pp. 210-225. This paper has also been presented at the Joint Workshops on Foundations of Computer Security (FCS02) and Verification (VERIFY02), Copenhagen, Denmark, July 25-26, 2002.
• A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. Mödersheim, M. Rusinowitch, M. Turuani, L. Viganò;, and L. Vigneron. The AVISS Security Protocol Analysis Tool. In the Proceedings of the 14th Conference on Computer-Aided Verification (CAV'02), pp. 249-353, Copenhagen, Denmark, July 27-31, 2002.
• A. Armando and P. De Lucia. Symbolic Model-Checking of Linear Programs. In the Proceedings of the 2nd Workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic (SAVE02), Copenhagen, Denmark, July 27, 2002.
• A. Armando, M. P. Bonacina, A. K. Sehgal, S. Ranise, and M. Rusinowitch. High-performance deduction for verification: a case study in the theory of arrays. In the Proceedings of the 2nd Verification Workshop (VERIFY02), pp. 103-112, Copenhagen, Denmark, July 25-26, 2002.
• A. Armando, M. Rusinowitch, S. Stratulat. Incorporating Decision Procedures in Implicit Induction In the Journal of Symbolic Computation (Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems) Vol. 34, No. 4, pp. 241-258, October, 2002.
• A. Armando, F. Peccia, S. Ranise. The Phase Transition of the Linear Inequalities Problem. In the Proceedings on the 7th International Conference on Principles and Practice of Constraint Programming (CP2001), Paphos, Cyprus, Nov 26 - Dec 1, 2001, pp. 422-432.
• A. Armando, S. Ranise, M. Rusinowitch. Uniform Derivation of Decision Procedures by Superposition. In the Proceedings on the Annual Conference on Computer Science Logic (CSL01), Paris, France, 10-13 September 2001, pp. 513-527.
• A. Armando, S. Ranise, M. Rusinowitch. A Superposition Based Methodology to Design Satisfiability Decision Procedures. In the Proceedings on the 5th International Workshop on Unification (UNIF'2001), Siena, Italy, 18-19 June 2001, pp. 8-12.
• A. Armando, C. Ballarin. Maple's Evaluation Process as Constraint Contextual Rewriting. In the Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC'2001), pp. 32-37, July 22-25, 2001, ORCCA and University of Western Ontario.
• A. Armando, M. Rusinowitch, S. Stratulat. Incorporating Decision Procedures in Implicit Induction. In the Proceedings of the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2001). Siena, June 21-22 2001, pp. 155-167.
• A. Armando, L. Compagna, S. Ranise. RDL---Rewrite and Decision procedure Laboratory. In the Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001), June 18-23, Siena, Italy. Lecture Notes in Artificial Intelligence, n. 2083, pp. 663-669.
• A. Armando, S. Ranise. A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. In the Journal of Universal Computer Science vol. 7:2, pp. 124-140, 2001. A short version of the paper has been presented at the 4th Workshop on Tools for System Design and Verification (FM-TOOLS 2000), p. 53-57. Reisenburg Castle near Ulm, Germany. Monday 10 July - Thursday 13 July 2000.
• A. Armando, A. Coglio, F. Giunchiglia, S. Ranise. The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics . In the Journal of Symbolic Computation (Special Issue on Calculemus-99: Integrating Computation and Deduction) Vol. 32, No. 4, October 1, 2001, pp. 305-332.
• J. Zimmer, A. Armando, C. Giromini. Towards Mathematical Agents -- Combining MathWeb-SB and LBA. In the Proceedings of the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2001). Siena, June 21-22 2001, pp. 64-77.
• A. Armando, S. Ranise. Termination of Constraint Contextual Rewriting. In the Proceedings of the 3rd International Workshop on Frontiers of Combining Systems (FroCoS'2000). Nancy (France), March 22-24, 2000. Lecture Notes in Computer Science, Volume 1794, pp. 47--61.
• A. Armando, M. Kohlhase, S. Ranise. Communication Protocols for Mathematical Services based on KQML and OMRS. In Symbolic Computation and Automated Reasoning. Proceedings of the Eight Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2000), St. Andrew (Scotland), 6-7 August 2000. M. Kerber and M. Kohlhase, editors, pag. 33-48. A K Peters Publisher, Natick, Massachussetts, 2001.
• A. Armando, D. Zini. Interfacing Computer Algebra and Deduction Systems via the Logic Broker Architecture. In Symbolic Computation and Automated Reasoning, proceedings of the Eight Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS-2000), St. Andrew (Scotland), 6-7 August 2000. M. Kerber and M. Kohlhase, editors, pag. 49-64. A K Peters Publisher, Natick, Massachussetts, 2001.
• A. Armando, C. Castellini, E. Giunchiglia. SAT-based procedures for temporal reasoning. In the Proceeding of the 5th European Conference on Planning (ECP-99). Durham (UK), September 8-10, 1999.
• A. Armando, A. Smaill, I. Green. Automatic Synthesis of Recursive Programs: the Proof-Planning Paradigm. In Automated Software Engineering, 6(4): 329-356, October 1999. Short version in the Proceedings of the 12th IEEE Conference on Automated Software Engineering - ASE'97, November 3 - 5, 1997. Lake Tahoe, Nevada; USA. Nominee for the best paper award.
• A. Armando, A. Coglio, F. Giunchiglia. The Control Component of Open Mechanized Reasoning Systems. In Electronic Notes in Theoretical Computer Science Volume 23, Issue 3, pp. 1--18, 1999.
• A. Armando, S. Ranise. Constraint Contextual Rewriting. In Proceedings of the International Workshop on First order Theorem Proving (FTP'98) pp. 65-75. Schloss Wilhelminenberg, Vienna, Austria November 23 - 25, 1998.
• A. Armando, J. Gallagher, A. Smaill, A. Bundy. Automating the Synthesis of Decision Procedures in a Constructive Metatheory. In the Annals of Mathematics and Artificial Intelligence vol. 22, n.3,4, pp. 259-279, 1998. Short version in the Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics, pp. 5--8, Florida, January 3-5, 1996.
• A. Armando, P. Bertoli, A. Coglio, F. Giunchiglia, J. Meseguer, S. Ranise, C. Talcott. Open Mechanized Reasoning Systems: a Preliminary Report. In the Proceedings of the CADE Workshop on Integration of Deduction Systems. July 5-6, 1998, Lindau, Germany.
• A. Armando, S. Ranise. From Integrated Reasoning Specialists to ``Plug-and-Play'' Reasoning Components. In Proceedings of the Fourth International Conference Artificial Intelligence and Symbolic Computation (AISC98) LNCS vol. 1476, p. 42-54. Plattsburgh, NY, USA. September 16-18, 1998.
• F. Giunchiglia, P. Pecchiari, A. Armando. Towards provably correct system synthesis and extension. In the Journal of Future Generation Computer Systems vol. 12, no. 2/3, p. 1-15, 1996.
• E.~Giunchiglia, A.~Armando, P.~Traverso, and A.~Cimatti. Visual Representation of Natural Language Scene Descriptions. In IEEE Transactions on Systems, Man and Cybernetics}, 26(04):575--589, 1996.
• E. Giunchiglia, A. Armando, P. Pecchiari. Structured Proof Procedures. In the Annals of Artificial Intelligence and Mathematics, vol. 15, n. 1, 1995.
• P. Traverso, A. Cimatti, L. Spalazzi, A. Armando, E. Giunchiglia. MRG: Building Planners for Real World Complex Applications. In Applied Artificial Intelligence, vol. 8, n. 3, p. 333-357, 1994.
• A. Armando, E. Giunchiglia. Embedding complex decision procedures inside an interactive theorem prover. In the Annals of Artificial Intelligence and Mathematics, vol. 8, n. 3-4, 1993.
• A. Armando, A. Cimatti, and L. Viganò. Building and Executing Proof Strategies in a Formal Metatheory. In Advances in Artificial Intelligence. Proc. AI*IA'93, number LNAI 728 in Lecture Notes in Artificial Intelligence, pp. 1--10, Torino, Italia, 26-28 Ottobre 1993. Springer Verlag.