Fabio Martinelli, Ph.D.
Senior researcher

ERCIM Working group in Security and Trust Management (STM)

New ERCIM STM WG 2009 Award for the Best Ph.D. Thesis

EC-ERCIM Strategic Seminar on Engineering Secure Complex Software Systems and Services

Join security@fosad.org, the mailing list (more than 600 addresses) for the scientific community interested in computer security research topics. Such a mailing list should serve as a forum for discussion and as a mean of quick dissemination of announcements of conferences and related events in the area of security.

Research Interests:

• Security
• Formal analysis of network and system security
• Security protocols
• Information flow analysis
• PKI and Trust management
• Access and Usage Control
• Run-time policy enforcement
• Distributed systems
• Formal analysis of concurrent/distributed/mobile systems
• Temporal logic: Model and module checking
• Program synthesis

Research Projects:

(current)

• EU-FET-IP Emergent Connectors for Eternal Software Intensive Networked Systems (CONNECT)
• EU-ICT-STREP Context-aware Information Sharing (Consequence).
• EU-IST-STREP Security and Trust for GRID systems (GRIDTrust).
• EU-FET-IP BIOlogically-inspired autonomic NETworks and Services (BioNets).
• EU-FET-IP on Software Engineering for Service-Oriented Overlay Computers (SENSORIA).
• EU-IST-NoE Embedded Systems (ARTIST2).
• MIUR ``BISCA" Biologically-inspired systems and calculi and their applications
• Tuscany Regional Government (VISITO) "Visual Sipport to cultural heritage InTerctive access in Tuscany"

(past)

• EU-IST-STREP Secure Software and Services for Mobile Systems (S3MS).
• NATO Advanced Training Course (ATC Dushanbe).
• CNR `` Trusted e-services for dynamic and mobile coalitions''
• MIUR ``SYBILLA" formal methods for the study of biological systems
• CREATE-NET ``Quality of Protection (QoP)''
• MURST ``Tools, techniques and methodologies for the information society''
• CNR ``Tecniche e Strumenti Software per l'analisi della sicurezza delle comunicazioni in applicazioni telematiche di interesse economico e sociale''
• CSP ``Metodi formali e strumenti per l'analisi automatica di protocolli di sicurezza (SeTAPS II)''
• MIUR ``Constraints for Verification (COVER)''
• MURST ``Formal Methods for Security and Time(MEFISTO)''
• EU ``Roadmaps for European research on Smartcard Technologies`` (RESET)
• Microsoft Research Europe (Cambridge) ``Security`` (by the way of Prof. R. Gorrieri)
• ESPRIT BRA ``Logical and Operational Methods in the Analysis of Programs and Systems''
• CNR Progetto Strategico ``Modelli e Metodi per la Matematica e l'Ingegneria'',
• MURST ``Tecniche Formali per la Specifica, l'Analisi, la Verifica e la Trasformazione dei Sistemi Software''.

Events

(current)

• International Symposium on Engineering Secure Software and Systems (ESSoS2010)
• ACM Symposium on Applied Computing (SAC'10) TRECK track: Trust, Recommendations, Evidence and other Collaboration Know-how (TRECK 10)
• ACM Symposium on Applied Computing (SAC'10) Track on Computer Security (9th edition)
• International Conference on Applied Cryptography and Network Security (ACNS)
• 25th IFIP International Information Security Conference (SEC 2010) Security & Privacy
• Workshop in Information Security Theory and Practice WISTP'10
• 6th International Verification Workshop – VERIFY-2010
• 6th International Workshop on Formal Aspects in Security and Trust(FAST09)
• 6th International Workshop on Public Key Services, Applications and Infrastructures (EUROPKI09)
• 12th Information Security Conference (ISC 2009)
• 5th International Workshop on Security and Trust Management (STM09)
• 9th International School in Foundations of Security Analysis and Design (FOSAD'09)
• IFIP International Conference on Trust Management (IFIPTM 2009)
• Inco-Trust: ICT Trust, Security and Privacy from six nations - EU, USA, Japan, Korea and Australia.
• 6th International Conference on Trust, Privacy & Security in Digital Business
• Dependable Computing and Communications Symposium (DSN-DCCS)
• WWW 2009 - Security Track
• 24th IFIP International information Security Conference (IFIP-SEC 2009)
• The First International ICST Conference on Security and Privacy in Mobile Information and Communication Systems
• ACM Symposium on Applied Computing (SAC'09) TRECK track: Trust, Recommendations, Evidence and other Collaboration Know-how (TRECK 09)
• ACM Symposium on Applied Computing (SAC'09) Track on Computer Security (8th edition)
• The Fourth International Conference on Information Assurance and Security (IAS 08)
• 4th International Workshop on Security and Trust Management (STM08)
• 4th ACM Workshop on QoS and Security for Wireless and Mobile Networks (Q2SWINET 2008).
• 5th International Workshop on Web Services and Formal Methods (WS-FM 08)
• 5th International Workshop on Formal Aspects in Security and Trust(FAST08)
• 8th International School in Foundations of Security Analysis and Design (FOSAD'08)
• 13th European Symposium on Research in Computer Security (ESORICS 2008)
• 16th Euromicro International Conference on Parallel, Distributed and network-based Processing (PDP 2008) - Special Session on "Security in Networked and Distributed Systems"
• The 2008 European PKI Workshop: Theory and Practice (EuroPKI'08)
• ACM Symposium on Applied Computing (SAC'08) TRECK track: Trust, Recommendations, Evidence and other Collaboration Know-how
• Symposium on Requirements Engineering for Information Security SREIS 2008
• IFIP International Conference on Trust Management (IFIPTM 2008)
• First International Workshop on Advances in Policy Enforcement (APE'08)
• First International Workshop on Security, Trust and Privacy in Grid Systems (Grid-STP 2007)
• 2nd Workshop EU/US Summit Series on Cyber Trust: System Dependability & Security
• 12th European Symposium on Research in Computer Security (ESORICS 2007)

(past)

My Bibliography

• 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
  • 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)
  • 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.

• 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.

Software Tools:

• PaMoChSA (Partial Model Checking Security Analyzer): A software tool for Computer aided verification of security protocols based on the idea of analyzing security protocols as open systems.
• SEAS (Secure E-voting Applet System): A software tool for E-voting/polling procedures through the web. This is based on an improvement of the SENSUS protocol.
• Secure applications for Smartphones A set of applications for smartphones based on cryptography and digital signature.

Teaching:

• MASTER in Internet Technologies (2004): Information Security
• Linguaggi e Calcolabilita'. A.A. 2004/2005. Corso di Laurea Specialistica in Tecnologie Informatiche.
• MASTER in Internet Technologies (2005): Information Security
• MASTER in Internet Technologies (2007): Information Security
• MASTER in Internet Technologies (2009): Information Security