• Edited Books/Journals

    • Special issue on the Journal of Theoretical Computer Science on Foundations of Security Analysis and Design (II), (con Roberto Gorrieri) vol 340-1, 2005.
    • Proceedings of the 2nd International workshop on Issues in Security with Petri Nets and other Computational Models (con N. Busi e R. Gorrieri) ENTCS, Volume 121, Pages 1-155 (4 February 2005).
    • Proceedings of the 2nd International workshop on Formal Aspects in Security and Trust (FAST2004) (con Theo Dimitrakos). Kluwer Academic Press August 22-27, 2004, Toulouse, France Series: IFIP International Federation for Information Processing, Vol. 173, 2005, 246 p., ISBN: 0-387-24050-0.
    • Foundations of Security Analysis and Design III (con A. Aldini e R. Gorrieri) Tutorial Lectures of the international research school on Foundations of Security Analysis and Design (Fosad 2004/2005). LNCS 3655, 2005.
    • Proceedings of the 3rd International workshop on Formal Aspects in Security and Trust (FAST2005) (con Theo Dimitrakos,Peter Y. A. Ryan, Steve Schneider ). Newcastle upon Tyne, UK, July 18-19, 2005, Revised Selected Papers Springer 2006.
    • Proceedings of the 4th International Conference on Trust Management (iTrust2006) (con Ketil Stoelen, Will H. Winsborough, Fabio Massacci). Pisa, Italy, May 16-19, 2006. LNCS 3986.
    • Special issue on the International Journal of Information Security on selected papers from FAST 2004/05. (con Theo Dimitrakos,Peter Y. A. Ryan, Steve Schneider ). Volume 6 number 2-3, March 2007.
    • Proceedings of the 5th International workshop on Formal Aspects in Security and Trust (FAST2008) (with P. Degano, J. D. Guttman). Revised Selected Papers Springer, LNCS 5491, 2009
    • Proceedings of the 12th Information Security, 12th International Conference ISC 09 (with Pierangela Samarati, Moti Yung, Claudio Agostino Ardagna), Pisa, Italy, September 7-9, 2009. Proceedings Springer 2009.
    • Special issue on Security and Trust in Dynamic Coalitions (with Theo Dimitrakos, Bruce Schneier). To appear in the Secure Communicaiton and Networks (Wiley)

  • Journals

    • An improvement of algorithms for solving interface equations. Information Processing Letters 67(4):185-190, 1998.
    • Analysis of security protocols as open systems. TCS 290(1): 1057-1106 (2003)
    • A comparison of three authentication properties (with R. Focardi and R. Gorrieri). TCS 291(3): 285-327 (2003).
    • Real Time information Flow Analysis (with R. Focardi and R. Gorrieri). IEEE JSAC 21(1), 2003.
    • A Simple Framework for Real-time Cryptographic Protocol Analysis with Compositional Proof Rules (con R. Gorrieri). Science of Computer Programming, Elsevier, Volume 50 , Issue 1-3 (2004).
    • Automated Analysis of Timed Security: a Case Study on Web Privacy (con Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo, Simone Tini e Enrico Tronci). International Journal of Information Security, volume 2, pp. 168 - 186, 2004.
    • Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis (con S. Bistarelli, I. Cervesato, G. Lenzini). Journal of Computer Security 13(1): 3-47 (2005).
    • SEAS: design and implmentation with Java applets. (con F. Baiardi, A. Falleni, R. Granchi, M. Petrocchi, A. Vaccarelli.) Computers\&Security, 24(8): 642-652 (2005).
    • Formal analysis of some secure procedures for certificate delivery (con M. petrocchi, A. Vaccarelli). Software, Testing, Verification and Reliability, Volume 16 (1),pp.33-59 (2006).
    • Constrained Finite State Automata for Risk Analysis and Assessment (con F.Baiardi, L.Ricci, C.Telmon). To appear in Journal of Information Assurance and Security.
    • Formal Models and Analysis of Secure Multicast in Wired and Wireless Networks (with R. Gorrieri, M. Petrocchi). Journal of Automated Reasoning. Volume 41 (3-4), pp. 325-364 (2008)
    • Enhancing grid security by fine-grained behavioral control and negotiation-based authorization (H. Koshutanski, A. Lazouski, and P.Mori) International Journal of Information Security. Volume 8, Number 4 / August, 2009
    • Runtime monitoring for next generation Java ME platform (with G. Costa, P. Mori, C. Schaeferb, and T. Walter) To appear in Computer&Security.
    • Securing Java with Local Policies (with M. Bartoletti1, G. Costa, P. Degano, and R. Zunino). To appear in Journal of Object Technology.

  • Book chapters/Tutorials

    • Classification of Security Properties -- Part II: Network security (with R. Focardi and R. Gorrieri). FOSAD school Lectures, volume 2946 of LNCS, 2004.
    • Security-by-Contract (SxC) for Software and Services of Mobile Systems (with N. Dragoni,F. Massacci, P. Mori, C. Schaefer, T. Walter and E. Vetillard). At your service: Servi- ce Engineering in the Information Society Technologies Program. MIT press (2008)
    • Usage Control for Trust and Security in Next Generation Grids (with P. Massonet, A. Arenas, P. Mori and B. Crispo). At your service: Service Engineering in the Information Society Technologies Program. MIT press (2008)
    • Enhancing Java Security with History Based Access Control (with F. Martinelli and P. Mori). Foundations of Security Ana- lysis and Design, Tutorial Lectures (FOSAD 2006/2007). Lecture Notes in Computer Science 4677: Springer Verlag (2007) 135–159
    • Formal techniques for security analysis in wireless systems (with M. Petrocchi). Security and Privacy in Mobile and Wireless Networking, ISBN: 978- 1905886-906. Troubador Publishing. Eds.: S. Gritzalis, T. Karygiannis, C. Skianis.
    • TRUST Management for GRID systems (with A. Arenas, B. Aziz, P. Mori, M. Petrocchi, M. Wilson.) to appear in 'Trust Modeling and Management in Digital Environments: from Social Concept to System Development, edited by Zheng Yan, published by IGI Global.

  • Conferences and Workshops

    • Languages for description and analysis of authentication protocols. In Proceedings of 6th Italian Conference on Theoretical Computer Science, Prato, Italy. World Scientific Press. 1998.
    • Partial model checking and theorem proving for ensuring security properties. In Proceedings of 11th Computer Security Foundations Workshop. Boston, (U.S). IEEE Computer Society Press, pages 44-52,1998.
    • Automatic verification of cryptographic protocols through compositional analysis techniques, (with Davide Marchignoli). In Proceedings of the International Conference on Tools and Algorithms for the Analysis and the Construction of Systems (TACAS), volume 1579 of Lectures Notes in Computer Science, pages 148--163, 1999.
    • A uniform approach for the definition of security properties, (with Riccardo Focardi). In Proceedings of the World Congress on Formal Methods, 1999, volume 1708 of LNCS, pages 794-814, 1999.
    • Secrecy in security protocols as non-interference, (with Riccardo Focardi and Roberto Gorrieri). Electronic Notes in Theoretical Computer Science 32, 2000.
    • Message authentication through non-interference, (with Riccardo Focardi and Roberto Gorrieri). In Proceedings of the 8th International Conference in Algebraic Methodologies and Software Technology. Iowa (US), May 2000.
    • Information flow analysis in a discrete-time process algebra, (with Riccardo Focardi and Roberto Gorrieri). In Proceedings of the 13th Computer Security Foundations Workshop. Cambridge (UK), July 2000.
    • Non-interference for the analysis of security protocols, (with Riccardo Focardi and Roberto Gorrieri). In Proceedings of the 27th International Colloquium in Automata, Languages and Programming. Geneve (CH), July 2000.
    • A case study with PaMoChSA: A tool for the automatic analysis of cryptographic protocols, (with A. Giani, M. Petrocchi, A. Vaccarelli). In Proceedings of the 5th SCI/ISAS conference (Network protocol track) . Orlando (U.S), July 2001.
    • Techniques for security analysis: Non-Interference vs. Control Flow Analysis, (with C. Bodei, P. Degano, R. Focardi, R. Gorrieri). In proceedings of Theory of Concurrency, Higher Order and Types Workshop. Volume 62 of ENTCS. Udine (Italy), 2001.
    • Formal modelling of time attacks, (with R. Focardi, R. Gorrieri, R. Lanotte, A. Maggiolo, E. Tronci, S. Tini). In proceedings of Theory of Concurrency, Higher Order and Types Workshop. Volume 62 of ENTCS. Udine (Italy), 2001.
    • About compositional analysis of pi-calculus processes. Accepted for publication in proceedings of the 2nd IFIP World conference on Theoretical Computer Science, 2002.
    • Symbolic semantics and analysis for Crypto-CCS with (almost) generic inference systems. Accepted for publication in the proceedings of the 27th Symposium in Mathematical Foundations of Computer Science (MFCS), 2002.
    • Automated analysis of some security mechanisms of SCEP (with M. Petrocchi and A. vaccarelli). To appear in proceedings of the Information Security Conference, San Paulo, Brazil, 2002.
    • A simple language for real-time cryptographic protocol analysis (with R. Gorrieri and E. Locatelli). Accepted for publication in the proceedings of the European Symposium on Programming (ESOP), 2003.
    • Compositional verification of integrity for digital stream signature protocols (with R. Gorrieri, M. Petrocchi, A. Vaccarelli) Accepted for publication in the procceding of the international conference on Application of Concurrency to System Design, IEEE Press, 2003.
    • Enhancing smart card security through biometry (A MOC protocol via TOC) (with G. Bella, S. Bistarelli). To appear in Proc. of the Cambridge Security Protocols Workshop, LNCS. 2003.
    • Symbolic partial model checking for security analysis. To appear in proc. of Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, LNCS, 2003.
    • Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis (with S. Bistarelli, I. Cervesato, G. lenzini). To appear in proc. of Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security, LNCS 2003.
    • Process Algebraic Frameworks for the Specification and Analysis of Cryptographic Protocols (with R. Gorrieri). To appear in Proc of MFCS, LNCS 2003.
    • Compositional Verification of Secure Streaming Data: a Case Study with EMSS, (with M. Petrocchi, A. Vaccarelli). To appear in proc. of ICTCS'03, LNCS, 2003.
    • On representing biological systems through Multiset rewriting (with with S. Bistarelli, I. Cervesato, G. lenzini, R. Marangoni). In Proc. of the 9th International Conference on Computer Aided Systems Theory (EUROCAST), LNCS, 2003.
    • Formal analysis of some security properties of wireless/sensor protocols, (with R. Gorrieri, M. Petrocchi, A. vaccarelli) To appear in proceedings of the FMOODS, LNCS, 2003.
    • Logical specification and analysis of fault tolerant systems through partial model checking (with S. Gnesi, G. Lenzini). In proc. of the International Workshop on Software Verification and Validation (SVV) 2003, ENTCS, Mumbai, India, 2003.
    • SEAS: Secure E-voting Applet System, (with F. Baiardi, A. Falleni, R. Granchi, M. Petrocchi, A. Vaccarelli). To appear in proc. of the 3rd International Symposium on Software Security, Tokyo, 2003, LNCS.
    • Applying the Non-Deducibility on Compositions Approach (GNDC) in Dependability (with S. Gnesi, G. Lenzini). In proc. of the Workshop on Formal Methods for Security and Time (MEFISTO), ENTCS, 2004.
    • A framework for locally managing credits and debits in MANETs (with M. Petrocchi and A. Vaccarelli) Eighth IFIP TC-6 TC-11 Conference on Communications and Multimedia Security. To appear, 2004.
    • Improving GRID security with fine grain policies (with F. Baiardi, P. Mori, A. Vaccarelli). To appear in proc. of 1st International Workshop on GRID Computing and its Applications to Data Analysis (GADA'04). To appear, LNCS, 2004.
    • A Flexible Framework for Access Control based on Ability Authentication (con F. Dianda, F. Giuntini, A. Vaccarelli). In proc. of Workshop on Network Security Threats and Countermeasures. To appear, IEEE press , 2005.
    • Towards an Integrated Formal Analysis for Security and Trust. To appear in proc. of FMOODS 2005. LNCS.
    • A Formalization of Credit and Responsibility within the GNDC schema (with R. Gorrieri and M. Petrocchi). In proc. of the 1st International Workshop on Security and Trust Management (STM'05), ENTCS, Volume 157, Issue 3, Pages 1-158.
    • Toward Continuous Usage Control on Grid Computational Services (with P. Mori and A. vaccarelli). In proc. of nternational Conference on Autonomic and Autonomous Systems and International Conference on Networking and Services. IEEE Press, 2005.
    • Fine-grained and History-based Access Control with Trust Management for Autonomic Grid Services (with H. Kostukanski, P. Mori and A. Vaccarelli). In proc. of ICAS'06. IEEE Press, 2006.
    • A Fine-grained Access Control System for Globus Based on X.509 Certificates (with H. Kostukanski, P. Mori and A. Vaccarelli and Luca Bortz). In proc. of the International Symposium on GRID Computing and its Applications to Data Analysis (GADA'06), LNCS 4276, 2006.
    • Constrained Finite State Automata for Risk Analysis and Assessment (con F.Baiardi, L.Ricci e C.Telmon). NATO Advanced Research Workshop on information Security Assurance and Security, Volume 6 NATO Security through Science Series: Information and Communication Security, November 2006. (ISBN: 1-58603-678-5)
    • On relating and integrating two trust management languages (with Marinella Petrocchi). In proc. of the 2nd International Workshop on Views On Designing Complex Architectures (VODCA'06). Electr. Notes Theor. Comput. Sci. 168: 191-205 (2007).
    • An Approach for the Specification, Verification and Synthesis of Secure Systems (with Ilaria Matteucci). In proc. of the 2nd International Workshop on Views On Designing Complex Architectures (VODCA'06). Electr. Notes Theor. Comput. Sci. 168: 29-43 (2007).
    • A Uniform Framework for Security and Trust Modeling and Analysis with Crypto-CCS (with M. Petrocchi). Electr. Notes Theor. Comput. Sci. 186: 85-99 (2007)
    • Extending the Globus Architecture with Role-Based Trust Management (with Maurizio Colombo, Fabio Martinelli, Paolo Mori, Anna Vaccarelli). EUROCAST 2007: 448-456
    • Access control mechanisms for fraglets (with M. Petrocchi). 2nd International Conference on Bio inspired Models of Network, Information and Computing Systems (BIONETICS 2007). ICST, 2007.
    • Fine Grained Access Control with Trust and Reputation Management for Globus (with M. Colombo, P. Mori, M. Petrocchi, A. Vaccarelli). International Conference on Grid computing, high-performAnce and Distributed Applications (GADA 2007). LNCS 4804. Springer, 2007.
    • A Model for Usage Control in GRID Systems (with P. Mori). In Proceeding of Grid-STP 2007, Interna- tional Workshop on Security, Trust and Privacy in Grid Systems at SecureComm 2007. IEEE Computer Society, (2007).
    • Synthesis of Web Services Orchestrators in a Timed Setting (with I. Matteucci). WS-FM 2007, LNCS 4937-0124.
    • Synthesis of local controller programs for enforcing global security properties (with I. Matteucci). IEEE International Workshop on Advances in Policy Enforcement (APE'08). IEEE Press.
    • Weighted Datalog and Levels of Trust (with S. Bistarelli, F. Santini) IEEE International Workshop on Advances in Policy Enforcement (APE'08). IEEE Press.
    • A Runtime Monitoring Environment for Mobile Java (with P. Mori, T. Quillinan, and C. Schaefer (DoCoMo)). 1st International ICST workshop on Security Testing. Lillehammer, Norway. 9 April 2008 (To Appear).
    • A Semantic Foundation for Trust Management Languages with Weights: An Application to the RTFamily (with S. Bistarelli, F. Santini). ATC 2008: 481-495
    • Mobile implementation and formal verification of an e-voting system (with S. Campanelli, A. Falleni, M.Petrocchi, A. Vaccarelli). The Third International Conference on Internet and Web Applications and Services (ICIW 2008). IEEE CS 2008.
    • Controlling Usage in Business Processes Workflows through Fine-Grained Security Policies (B. Aziz, A. Arenas, F. Martinelli, I Matteucci, P Mori). Proc. 5th International Conference on Trust, Privacy & Security in Digital Business (TrustBus 2008), Turin, Italy, 01-05 Sep 2008, Lecture Notes in Computer Science, Vol. 5185, Springer
    • Enhancing Java ME Security Support with Resource Usage Monitoring (with P. Mori, A. Castrucci and F. Roperti). ICICS 2008, to appear in LNCS.
    • A Framework for Contract-Policy Matching based on Symbolic Simulations for securing Mobile Device Application (with P. Greci and I. Matteucci). In proc. 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Springer 2008.
    • Fine-grained Continuous Usage Control of Service based Grids – The GridTrust Approach (with S. Naqvi, P. Massonet, B. Aziz, A. Arenas, F. Martinelli, P. Mori, L. Blasi, G. Cortese). ServiceWave2008, to appear on LNCS.
    • Towards information flow properties for distributed systems (with R. Gorrieri adn I. Matteucci). VODCA 2008, to appear on ENTCS.
    • On usage control in data GRIDs (wit. F. Stagni. A. Arenas and B. Aziz). To appear in procs. of IFIP TM 2009.
    • A proposal on enhancing XACML with continuous usage control features (with A. Lazouski, M. Colombo, P. Mori). CoreGRID ERCIM Working Group Workshop on Grids, P2P and Service computing, in Conjunction With EuroPAR 2009
    • On Usage Control for GRID Services (with A. Lazouski, M. Colombo, P. Mori) 2009, IEEE International Workshop on HPC and Grid Applications (IWHGA2009) in conjunction with The 2009 International Symposium on Applied Computing and Computational Sciences (ACCS 2009)
    • Detection of Images with Adult Content for Parental Control on Mobile Devices (with G. Amato, P. Bolettieri, G. Costa, F. la Torre) ACM Mobility Conference, 2009.
    • Resource access in Multi-Provider Networks using Role Based Trust Management (with P. Mori, M. Colombo, B. Martini, F. Baroncelli and P. Castoldi). To appear in ENTCS.
    • Executable specification of cryptofraglets in Maude for security verification (with M. Petrocchi). To appear in BIONETICS 2009.
    • Secure Service Composition with Symbolic Effects (with G. Costa, P. Degano) 4th South-East European Workshop on Formal Methods, 2009. To appear.
    • Extending security-by-contract with quantitative trust on mobile devices (with G. Costa, N. Dragoni, A. Lazouski, F. Massacci, and I.Matteucci.). In IMIS'10: Proceedings of the 4th International Workshop on Intelligent, Mobile and Internet Services in Ubiquitous Computing, 2010. To appear.
    • Risk-Based Usage Control for Service Oriented Architecture (with L. Krautsevich, A. Lazouski, and A. Yautsiukhin). To appear in Proceedings of The 18th Euromicro International Conference on Parallel, Distributed and Network-Based Computing (PDP 10).

  • Presentations in international workshops with review process

    • A uniform approach for the solution of module checking problems. Presented at the Workshop on Distributed Systems, Iasi, Romania, 1999.
    • A uniform approach for the analysis of cryptographic protocols, (with Riccardo Focardi). Presented at the 2nd Workshop on Security in Communication Networks, Amalfi, Italy, 1999.
    • Towards automatic synthesis of systems without informations leaks. Presented at the Workshop in Issues on Theory of Security, Geneva, CH, 2000.
    • Symbolic partial model checking for security analysis. To be presented at the Specification, Analysis and Verification Workshop (SAVE), Copenaghen, 2002.
    • Modeling and analyzing authentication through the inspection of the intruder knowledge. To appear in Proc. of the 9th international conference on Computer Aided Systems Theory (EUROCAST) 2003.
    • Compositional reasoning and non-interference for checking integrity in stream protocols (with M. Petrocchi, A. vaccarelli). To appear in proc. of the 3rd} International Workshop in Issues on Theory of Security (WITS), 2003.
    • Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis (with S. Bistarelli, I. Cervesato, G. lenzini). To appear in proc. of the 3rd International Workshop in Issues on Theory of Security (WITS), 2003.
    • SEAS, an improvement of the Sensus protocol: design and implementation (extended abstract), (with F. Baiardi, A. Falleni, R. Granchi, M. Petrocchi, A. Vaccarelli). 4 - th EUROPEAN CONFERENCE E-COMM-LINE 2003, Bucharest, September 2003.
    • A Formalization of Credit and Responsibility (with R. Gorrieri and M. Petrocchi) To appear in proc. of SASYFT 2004.
    • Managing Credits in Mobile Ad Hoc Networks (with M. Petrocchi, A. Vaccarelli). To be presented at the 2nd Workshop on Ubiquitious Networking (UK-Ubinet), Cambridge, May 5-7 2004.
    • Towards an Integrated Formal Analysis for Security and Trust. To be presented at the 2nd Workshop on Ubiquitious Networking (UK-Ubinet), Cambridge, May 5-7 2004.
    • Partial model checking, process algebra operators and satisfiability procedures for (automatically) enforcing security properties (con I. Matteucci). Foundations of Computer Security (FCS 2005).
    • Modeling security automata with process algebras and related results (with Ilaria Matteucci). In proc. of the 6th International Workshop in Issues on Theory of Security (WITS), 2006.
    • Extending Globus authorization with Role-based trust management (with Maurizio Colombo, Paolo Mori, Anna Vaccarelli). GRID Computing Workshop, EUROCAST 2007.
    • Securing Java with Local Policies (with Massimo Bartoletti1, Gabriele Costa, Pierpaolo Degano, and Roberto Zunino). 10th Workshop on Formal Techniques for Java-like Programs FTfJP 2008 Paphos, Cyprus; July 8, 2008.

    Ph.D. Thesis

    • Formal methods for the analysis of open systems with applications to security properties. Ph.D. Thesis, University of Siena, Feb. 1999.

  • Technical Reports

    • Encoding several security properties as properties of the intruder's knowledge. Technical Report IAT-B4 20/2001.
    • Module checking through partial model checking. Technical Report IIT-TR 06/2002.
    • Access control: AAAA where the first two As stand for Ability Authentication (con Fabio Dianda, Filippo Giuntini, Anna Vaccarelli). Technical report IIT 2004.
    • Realizzazione di un applicazione per l'incremento della sicurezza dei dispositivi mobili,(with Alessandro Falleni and Carlo Vallati). Technical report IIT-2006-B4-05.
    • Model and Synthesize Security Automata, (with Ilaria Matteucci). Technical report IIT-2006-TR-04.
    • Extending the Globus architecture with Role-Based Trust Management (with Maurizio Colombo, Paolo Mori and Anna Vaccarelli). Technical report 2006-TR-05.
    • Fine Grained Access Control for Computational Services, (with Paolo Mori and Anna Vaccarelli). Technical report IIT-2006-TR-06.
    • A Survey on Usage Control in Computer Security (with Aliaksandr Lazouski, Paolo Mori and Anna Vaccarelli). Technical report IIT-2008-TR-14.

    Other

    • Security: Formal Methods at Work (with S. Bistarelli and M. Petrocchi), ERCIM news 49 (Special Theme: Information Security), April 2002.
    • Integrating Digital Signature with biometric Information (with L. Bechelli, S. Bistarelli, M. Petrocchi, A. Vaccarelli). ERCIM news 49 (Special Theme: Information Security), April 2002.
    • Introduction: Special theme on security and trust management (with J-J Quisquater) ERCIM News 63. 2005
    • Formal Modelling and Verification in Service-Oriented Computing (with Maurice ter Beek, Stefania Gnesi, Franco Mazzanti and Marinella Petrocchi). ERCIM News 70, 2007.