Papers 
Foundations of Sotware Engineering 
  • Coordination Languages and Models
  • Service-Oriented Computing
    • Theory of Concurrency 
  • ST semantics
  • Action Refinement
  • Petri Nets and Other Models of Concurrency
  • Bio-inspired Models for Systems Biology
  • Miscellaneous
    • Security 
  • Theory of Information Flow Security
  • Analysis of Crypto-protocols
  • Applications
    • Real-Time and Performance Evaluation 
  • Timed and Real-time Models
  • Theory of Stochastic Process Algebras and Stochastic Petri Nets
  • Applications of SPA
    • Some Papers 

    Coordination Languages and Models 

    Supporting Secure Coordination in SecSpaces 
    R.Gorrieri, R.Lucchi, G.Zavattaro. 
    Fundamenta Informaticae 73(4):479-506, 2006. 

    Quantitative Information in the Tuple Space Coordination Model 
    M. Bravetti, R. Gorrieri, R. Lucchi, G. Zavattaro. 
    Theoretical Computer Science, 346(1):28-57, 2005. 

    Comparing Three Semantics for Linda-like Languages. 
    N.Busi, R.Gorrieri and G.Zavattaro. 
    Theoretical Computer Science 240(1):49-90, 2000. 

    On the Expressiveness of Linda Coordination Primitives. 
    N.Busi, R.Gorrieri and G.Zavattaro. 
    Information and Computation 156(1-2):90-121, 2000. 

    A Process Algebraic View of Linda Coordination Primitives. 
    Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro. 
    Theoretical Computer Science, volume 192(2), pag. 167-199, February 1998. 

    On the Expressiveness of Probabilistic and Prioritized Data-retrieval in Linda. 
    Mario Bravetti, Roberto Gorrieri, Roberto Lucchi, Gianluigi Zavattaro. 
    In procs. SeccCo'04, Electr. Notes Theor. Comput. Sci. 128(5): 39-53 (2005). 

    Probabilistic and Prioritized Data Retrieval in the Linda Coordination Model. 
    Mario Bravetti, Roberto Gorrieri, Roberto Lucchi, Gianluigi Zavattaro. 
    In procs. Coordination'04, LNCS 2949, pages 55-70, 2004. 

    SecSpaces: a Data-driven Coordination Model for Environments Open to Untrusted Agents 
    N.Busi, R.Gorrieri, R.Lucchi, G.Zavattaro. 
    In procs. 1st Int.l Workshop on Foundations on Coordination Languages and Software Architectures  
    (Foclasa) ENTCS 68.3, Brno, August 2002. 

    Models for Coordinating Agents: A Guided Tour 
    N.Busi, P.Ciancarini, R.Gorrieri, G.Zavattaro. 
    In "Coordination of Internet Agents: Models, Technologies and Applications"  
    (A.Omicini, P.Zambonelli, M.Klusch, R.Tolksdorf eds.), Springer, pages 6-24, 2001. 

    Temporary Data in Shared Dataspace Coordination Languages 
    N.Busi, R.Gorrieri, G.Zavattaro. 
    In procs. Fossac'01, LNCS 2030, 121-136, Springer, 2001. 

    On the Semantics of Javaspaces 
    N.Busi, R.Gorrieri, G.Zavattaro. 
    In procs. Formal Methods for Open Object-Based Distributed Systems IV (FMOODS'00) 
    (C.L. Talcott, F.S. Smith eds.), Kluwer, 3-19, Stanford (CA), September 2000. 

    Process Calculi for Coordination: from Linda to JavaSpaces 
    N.Busi, R.Gorrieri, G.Zavattaro. 
    In procs. Eighth Int.l Conference on Algebraic Methodology and Software Technology (AMAST'00) 
    LNCS 1816, Springer, pages 198-212, 2000. 

    On the Turing Equivalence of Linda Coordination Primitives. 
    Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro. 
    In proceedings of the Fourth Workshop on Expressiveness in Concurrency, EXPRESS 97. 

    Three Semantics of the Output Operation for Generative Communication. 
    Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro. 
    In Proceedings of the Second International Conference on Coordination Models and Languages, Coordination 97, 
    pag. 205-219, volume 1282 of Lecture Notes in Computer Science, Springer Verlag, 1997. 

    A Truly Concurrent View of Linda Interprocess Communication. 
    Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro. 
    Technical Report UBLCS-97-02, Department of Computer Science, University of Bologna, February 1997. 

    An Alternative Semantics for the Parallel Operator of the Calculus of Gamma Programs. 
    Paolo Ciancarini, Roberto Gorrieri, Gianluigi Zavattaro. 
    In  Coordination Programming: Mechanism, Models and Semantics, pag. 232-248, Imperial College Press, February 1996. 

    Towards a Calculus for Generative Communication. 
    Paolo Ciancarini, Roberto Gorrieri, Gianluigi Zavattaro. 
    In Proceeding of the First IFIP Conference on Formal Methods for Open Object-based Distributed Systems, FMOODS'96, 
    pag. 283-297, Chapman & Hall, March 1996. 
     


    Back to Top

    Service-Oriented Computing 

    SOCK: A Calculus for Service Oriented Computing. 
    Claudio Guidi, Roberto Lucchi, Roberto Gorrieri, Nadia Busi, Gianluigi Zavattaro. 
    In procs. Fourth Int.l Conference on Service-Oriented Computing (ICSOC'06),
    LNCS 4294, pages 327-338, Chicago, 2006. 

    Choreography and Orchestration Conformance for System Design 
    Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, Gianluigi Zavattaro. 
    In procs. Coordination 2006, LNCS 4038, pages 63-81, Bologna 2006. 

    Choreography and Orchestration: A Synergic Approach for System Design. 
    Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, Gianluigi Zavattaro. 
    In procs. Third Int.l Conference on Service-Oriented Computing (ICSOC'05), LNCS 3826, pages 228-240, Amsterdam, 2005. 

    Reasoning About Interaction Patterns in Choreography. 
    Roberto Gorrieri, Claudio Guidi, Roberto Lucchi. 
    In procs. Int.l Workshop on Web Services and Formal Methods (WS-FM'05), LNCS 3670, pages 333-348, 2005. 

    Towards a formal framework for Choreography. 
    Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, Gianluigi Zavattaro. 
    In procs. 14th IEEE Int.l Workshops on Enabling Technologies (WETICE 2005), Linköping, Sweden. 
    IEEE Computer Society, pages 107-112, 2005. 

    Web Services for E-commerce: guaranteeing security access and quality of service. 
    Mario Bravetti, Roberto Lucchi, Gianluigi Zavattaro, Roberto Gorrieri. 
    In procs. ACM Symposium on Applied Computing (SAC'04), ACM Press, pages 800-806, 2004.


    Back to Top

    ST Semantics 

    Deciding and Axiomatizing ST Bisimulation for a Process Algebra with Recursion and Action Refinement. 
    M.Bravetti,R.Gorrieri. 
    ACM Transactions on Computational Logic (TOCL), volume 3(4):465-520, 2002. 

    Split and ST Bisimulation Semantics. 
    R. Gorrieri, C. Laneve. 
    Information and Computation, volume 118 (2), pagine 272-288, 1995. 

    Axiomatizing ST Bisimulation for a Process Algebra with Recursion and Action Refinement (Extended Abstract) 
    M.Bravetti, R.Gorrieri. 
    in Proc. 6th Int. Workshop on Expressiveness in Concurrency (EXPRESS'99), ENTCS 27, Eindhoven, August 1999.  

    Axiomatising ST Bisimulation Equivalence. 
    Nadia Busi, Rob van Glabbeek and Roberto Gorrieri. 
    In Proc. IFIP Working Conference on Programming Concepts, Methods and Calculi, S. Miniato, June 1994. 

    An Extensional Formulation of ST  Bisimulation. 
    R. Gorrieri and C. Laneve. 
    In Proc. of Quarta Conferenza Italiana di Informatica Teorica. 
    A. Marchetti Spaccamela and M. Venturini Zilli eds., World Scientific, pag. 239-253, October 1992. 

    The Limit of Split$_{n}$-Bisimulations for CCS Agents. 
    R. Gorrieri and C. Laneve. 
    In Proc. of sixteenth International Symposium on Mathematical Foundations of Computer Science (MFCS 91), 
    A. Tarlecki ed., LNCS 520, Springer-Verlag, pag. 170-180, Kazimierz Dolny (Polonia), September 1991. 


    Back to Top

    Action Refinement 

    Action Refinement. 
    R.Gorrieri, A. Rensink. 
    Chapter XVI of Handbook of Process Algebra, (J. Bergstra, A. Ponse, S. Smolka eds), Elsevier, 1047-1147, 2001. 

    Vertical Implementation. 
    A.Rensink, R.Gorrieri. 
    Information and Computation 170(1):95-133, 2001. 

    Comparing Syntactic and Semantic Action Refinement. 
    U. Goltz, R. Gorrieri  and A. Rensink. 
    Information and Computation, volume 125 (2):118-143, 1996. 

    A Causal Operational Definition of Action Refinement. 
    P. Degano, R. Gorrieri. 
    Information and Computation, volume 122 (1), pagine 97-119, 1995. 

    A Hierarchy of System Descriptions via Atomic Linear Refinement. 
    R. Gorrieri. 
    Fundamenta Informaticae, volume 16(3/4):289-336, 1992. 

    Action Refinement for Vertical Implementation. 
    R.Gorrieri and A.Rensink. 
    In Proc. of Formale Beschreibungstechniken fur verteilte Systeme (FBT'97). 
    Organized by GI/ITG Fachgruppe Kommunikation und Verteilte Systeme, 
    GMD-FOKUS, Berlin (D), June 1997. 

    Action Refinement as an Implementation Relation. 
    R.Gorrieri and A.Rensink. 
    In Proc. of Colloquium on Formal Approaches in Software Engineering (FASE), 
    M.Bidoit e M.Dauchet eds., LNCS 1214, pag. 772-786, Springer-Verlag, Lille (France), April 1997. 

    On Syntactic and Semantic Action Refinement. 
    U. Goltz, R. Gorrieri and A. Rensink. 
    In Proc. of International Conference on Theoretical Aspects of Computer Software (TACS'94), 
    M. Hagiya and J.C. Mitchell eds., LNCS 789, Springer-Verlag, pag. 385-404, Sendai (Japan), April 1994. 

    A Categorical View of Process Refinement. 
    P. Degano, R. Gorrieri and G. Rosolini. 
    In Proc. of REX Workshop on Semantics: Theory and Applications, 
    J. de Bakker, G. Rozenberg and J. Rutten eds., June 1992, 
    LNCS 666, Springer-Verlag, pag. 131-153, Beekbergen (The Netherlands), June 1992. 

    Operational Definitions of Action Refinement based on Semantic Substitution. 
    Ph. Darondeau, P. Degano and R. Gorrieri. 
    In Proc. of Third Workshop on Concurrency and Compositionality, 
    E. Best ed., pag. 57-62, Goslar-Harz (Germany), March 1991. 

    Atomic Refinement for Process Description Languages. 
    P. Degano and R. Gorrieri. 
    In Proc. of sixteenth International Symposium on Mathematical 
    Foundations of Computer Science (MFCS 91), 
    A. Tarlecki ed., LNCS 520, Springer-Verlag, pag. 121-130, Kazimierz Dolny (Polonia), September 1991. 


    Back to Top

    Petri Nets and Other Models of Concurrency 

    Distributed Semantics for the pi-calculus based on Petri nets with inhibitor arcs 
    N. Busi and R. Gorrieri. 
    Journal of Logic and Algebraic Programming, 78(3):138-162, 2009  

    On the Implementation of Concurrent Calculi in Net Calculi: Two Case Studies. 
    R. Gorrieri and U. Montanari. 
    Theoretical Computer Science, volume 141(1-2):195-252, 1995. 

    On the Relationship between pi-calculus and Finite Place/Transition Petri Nets  
    Roland Meyer  and Roberto Gorrieri. 
    In Proc. 20th International Conference on Concurrency Theory (CONCUR'09), LNCS 5710, pages 463-480, Springer, Bologna, September 2009. 

    A Petri Net Semantics for pi-calculus.  
    Nadia Busi  and Roberto Gorrieri. 
    In Proc. 6th International Conference on Concurrency Theory (CONCUR'95), Philadelphia, August 1995. 

    On Relating Some Models for Concurrency. 
    P. Degano, R. Gorrieri, S. Vigna. 
    In Proc. of Theory and Practice of Software Technology (TAPSOFT'93), 
    M.-C. Gaudel and J.-P. Jouannaud eds., LNCS 668, Springer-Verlag, pag. 15-30, Orsay (France), April 1993. 

    Distributed Implementation of CCS. 
    R. Gorrieri and U. Montanari. 
    In Advances in Petri Nets 1993, G. Rozenberg ed., LNCS 674, Springer-Verlag, pag. 244-266. 
    Extended abstract negli atti di Twelfth International Conference on 
    Applications and Theory of Petri Nets, pag. 329-348, Gjern (Danimarca), Giugno 1991. 

    A Simple Calculus of Nets. 
    R. Gorrieri and U. Montanari. 
    In Proc. of CONCUR 90, Theories of Concurrency: Unification and Extension, 
    J.C.M. Baeten and J.W. Klop eds., LNCS 458, Springer, pag. 2-30, Amsterdam (The Netherlands), August 1990. 

    An Exercise in Concurrency: A CSP Process as a Condition/Event System. 
    P. Degano, R. Gorrieri and S. Marchetti. 
    Advances in Petri Nets 1988, G. Rozenberg ed., LNCS 340, Springer-Verlag, pag. 85-105, 1988. 
    Extended abstract in Proc. of Eighth European Workshop on Applications 
    and Theory of Petri Nets, pag. 31-50, Saragozza (Spain), June 1987. 

    A Distributed, Net Oriented Semantics for Delta Prolog. 
    A. Brogi and R. Gorrieri. 
    In Proc. of Theory and Practice of Software Development - Colloquium on Trees in Algebra and Programming (TAPSOFT 89), 
    J. Diaz and F. Orejas eds., LNCS 351, Springer-Verlag, pag. 162-177, Barcellona (Spain), March 1989. 


    Back to Top

    Bio-inspired Models for Systems Biology 

    pi@: A pi-based process calculus for the implementation of compartimentalised bio-inspired calculi. 
    Cristian Versari and Roberto Gorrieri. 
    Formal Methods for Computational Systems Biology, LNCS 5016, pages 449-506 (2008). 

    On the Computational Power of Brane Calculi 
    Nadia Busi, Roberto Gorrieri. 
    Transactions on Computational Systems Biology IV, LNCS 4220, pages 16-43 (2006). 


    Back to Top

    Miscellaneous 

    An expressiveness study of priority in process calculi. 
    Cristian Versari, Nadia Busi, Roberto Gorrieri.  
    Mathematical Structures in Computer Science, 19(6):1161-1189, 2009.  

    Ugo Montanari and Concurrency Theory 
    R.Gorrieri.  
    Concurrency, Graphs and Models: Essay dedicated to Ugo Montanari, LNCS 5065, 403-408, Springer, 2008.  

    On the expressive power of Local and Global Priority in Process Algebra. 
    Cristian Versari, Nadia Busi, Roberto Gorrieri.  
    in Procs. CONCUR 2007, LNCS 4703, 241-255, Springer, 2007.  

    Towards Parallelization of Concurrent Systems 
    F.Corradini, R.Gorrieri and D.Marchignoli, 
    RAIRO Informatique Theorique et Applications, 32(4-6):99-125, 1998. 

    On the Power of Concurrency Theory. 
    R. Gorrieri. 
    Position statement of the ACM Workshop Strategic Directions in Computing, 
    Electronic ACM Computing Survey, volume 28 (4es),  
    article 42, 1996. 

    Distributed Logic Programming. 
    A. Brogi and R. Gorrieri. 
    Journal of Logic Programming, volume 14(4):295-335, 1993. 

    Towards Hierarchical Specification of Systems: A Proof System for Strong Prefixing. 
    R. Gorrieri and U. Montanari, 
    Int. Journal of Foundations of Computer Science, volume 1(3):277-293, 1990. 

    A^2CCS: Atomic Actions for CCS. 
    R. Gorrieri, S. Marchetti and U. Montanari. 
    Theoretical Computer Science, volume 72:203-223, 1990. 

    A Complete Axiomatisation for Observational Congruence of Prioritized Finite-State Behaviours. 
    M.Bravetti, R.Gorrieri. 
    In procs. International Colloquium on Automata, Languages and Programming (ICALP'00) 
    LNCS 1853, 744-755, Springer, July 2000. 

    Distributed Conflicts in Communicating Systems. 
    N. Busi and R. Gorrieri. 
    In Object-Based Models and Languages for Concurrent Systems, 
    P. Ciancarini, O. Nierstrasz and A. Yonezawa eds., LNCS 924, Springer-Verlag, pag. 49-65, 
    Extended abstract in Proc. of ECOOP'94 Workshop on Models and Languages for Coordination of 
    Parallelism and Distribution, Bologna (Italy), July 1994. 

    The Kernel of a Graphic Environment for Analyzing Distributed Systems. 
    P. Degano, R. Gorrieri, L. Zamboni and P. Zanotti. 
    In Proc. of Parallel Computer Technologies (PaCT'91) - UNESCO Conference, 
    N.N. Mirenkov ed., World Scientific, pagine 266-279, Novosibirsk (Russia), September 1991. 

    An Extended Expansion Theorem. 
    G.L. Ferrari, R. Gorrieri and U. Montanari. 
    In Proc. of TAPSOFT 91, Theory and Practice of Software Development, 
    S. Abramski and T.S.E. Maibaum eds., LNCS 494, Springer-Verlag, pag. 29-48, Brighton (UK), April 1991. 
    Implicative Formulae in the `Proofs as Computations' Analogy. 
    A. Asperti, G.L. Ferrari and R. Gorrieri. 
    In Proc. of sixteenth Annual ACM Symposium on Principles of Programming Languages (POPL 90), 
    ACM Press, pag. 59-71, San Francisco (CA), January 1990. 

    Two Level Semantics for Process Description Languages: A Proof System for Strong Prefixing. 
    R. Gorrieri and U. Montanari. 
    In Proc. of Terza Conferenza Italiana di Informatica Teorica, 
    A. Bertoni, C. Bohm and P. Miglioli eds., World Scientific, pag. 311-322, November 1989. 

    Model Theoretic, Fixpoint and Operational Semantics for a Distributed Logic Language. 
    A. Brogi and R. Gorrieri. 
    In Proc. Sixth International Conference on Logic Programming, 
    G. Levi and M. Martelli eds., MIT Press, pag. 637-654, Lisbon (Portugal), June 1989. 

    A$^{2}$CCS: A Simple Extension of CCS for Handling  Atomic Actions. 
    R. Gorrieri, S. Marchetti e U. Montanari, 
    In Proc. Colloquium on Trees in Algebra and Programming 1988 (CAAP 88), 
    M. Dauchet and M. Nivat eds., LNCS 299, Springer-Verlag, pag. 258-270, Nancy (Francia), March 1988. 
     


    Back to Top

    Theory of Information Flow Security 

    Structural Non-Interference in Elementary and Trace nets 
    N. Busi and R.Gorrieri. 
    Mathematical Structures in Computer Science, 19(6):1065-1090, 2009. 

    A Process Algebraic Approach for the Analysis of Probabilistic Non-Interference 
    A.Aldini, M.Bravetti, R.Gorrieri. 
    Journal of Computer Security 12(2):191-245, 2004. 

    Automated Analysis of Timed Security: A Case Study on Web Privacy 
    R.Gorrieri, R.Lanotte, A.Maggiolo-Schettini, F.Martinelli, S.Tini, E.Tronci. 
    International Journal of Information Security 2(3-4):168-186, 2004. 

    Real-time Information Flow Analysis. 
    R.Focardi, R.Gorrieri, F.Martinelli. 
    Journal of Selected Areas of Communications (JSAC), volume 21(1):18-32, 2003. 

    The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. 
    Riccardo Focardi and Roberto Gorrieri. 
    IEEE Transactions on Software Engineering , Vol. 23, No. 9, September 1997. 

    A Classification of Security Properties for Process Algebras. 
    Riccardo Focardi and Roberto Gorrieri. 
    Journal of Computer Security , 3(1): 5-33, 1995. 

    On Itransitive Non-interference in some Models of Concurrency. 
    Roberto Gorrieri and Matteo Vernali. 
    Isubmitted, january 2009. 

    Petri Net Security Checker: Structural Non-interference at Work. 
    Simone Frau, Roberto Gorrieri and Carlo Ferigato. 
    In procs Formal Aspects of Security and Trust, LNCS 5491, pages 210-225, Springer, 2009. 

    Towards Information Flow for Distributed Systems. 
    Roberto Gorrieri, Fabio Martinelli and Ilaria Matteucci. 
    In procs VODCA'08, ENTCS 236:65-84, 2009. 

    Positive Non-interference in Elementary and Trace Nets. 
    Nadia Busi, Roberto Gorrieri. 
    In procs 25th Int.l Conf. on Applications and Theory of Petri Nets (ICATPN'04), LNCS 3099, pages 1-16, 2004. 

    A Survey on Non-Interference with Petri Nets 
    N.Busi, R.Gorrieri. 
    In Advanced Course on Petri Nets 2003, LNCS 3098, Springer, 328-344, 2004. 

    Structural Non-interference with Petri Nets 
    N.Busi, R.Gorrieri. 
    In procs. Fourth Workshop on Issues in the Theory of Security (WITS '04), 2004. 

    Two Formal Approaches for Approximating Noninterference Properties
    A.Aldini, M.Bravetti, A.Di Pierro, R.Gorrieri, C.Hankin, H.Wiklicky.. 
    In "Foundations of Security Analysis and Design II", LNCS 2946, 1-43, Springer, 2004. 

    Classification of Security Properties. Part I: Information Flow 
    R.Focardi, R.Gorrieri. 
    In "Foundations of Security Analysis and Design I", LNCS 2171, pages 331-396, Springer, 2001. 

    Information Flow Analysis in a Discrete Time Process Algebra 
    R.Focardi, R.Gorrieri, F.Martinelli. 
    In procs. 13th IEEE Computer Security Foundations Workshop (CSFW13)}, IEEE CS Press, 170-184, 2000. 

    A New Definition of Multilevel Security 
    Riccardo Focardi, Roberto Gorrieri, Roberto Segala. 
    In procs. Workshop on Issues in the Theory of Security (WITS '00), Ginevra, July 2000. 

    Non Interference: Past, Present and Future. 
    Riccardo Focardi and Roberto Gorrieri. 
    In Proceedings of DARPA Workshop on Foundations for Secure Mobile Code , 26-28 March 1997 Monterey, California, USA. 

    Automatic Compositional Verification of Some Security Properties. 
    Riccardo Focardi and Roberto Gorrieri. 
    In Proceedings of Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems 
    (TACAS'96), (B. Steffen Ed.), pages 167-186, Passau (Germany), March 1996. Springer-Verlag, LNCS 1055. 

    The Security Checker: a Semantics-based Tool for the Verification of Security Properties. 
    Riccardo Focardi, Roberto Gorrieri and Villiam Panini. 
    In Proceedings of Eighth IEEE Computer Security Foundations Worhshop (CSFW'95), (Li Gong Ed.), 
    IEEE Press, pages 60-69, Kenmare (Ireland), June 1995. 

    A Taxonomy of Trace-based Security Properties for CCS. 
    Riccardo Focardi and Roberto Gorrieri. 
    In Proceedings of Seventh IEEE Computer Security Foundations Workshop (CSFW'94), (Li Gong Ed.), 
    IEEE Press, pages 126-136, Franconia (NH), June 1994. 

    An Information Flow Security Property for CCS. 
    Riccardo Focardi and Roberto Gorrieri. 
    In Proceedings of Second North American Process Algebra Workshop (NAPAW'93), (B. Bloom Ed.), 
    TR-93/1369 of Cornell University, Ithaca (NY), August 1993. 
     


    Back to Top

    Analysis of Crypto-protocols 

    Formal Models and Analysis of Secure Multicast in Wired and Wireless Networks 
    R.Gorrieri, F.Martinelli, M. Petrocchi. 
    Journal of Automated Reasoning, to appear, 2008. 

    A Simple Framework for Real-time Cryptographic Protocol Analysis with Compositional Proof Rules 
    R.Gorrieri, F.Martinelli. 
    Science of Computer Programming 50(1-3):23-49, 2004. 

    A Comparison of Three Authentication Properties. 
    R.Focardi, R.Gorrieri, F.Martinelli. 
    Theoretical Computer Science, volume 291(3):285--327, 2003. 

    A Compiler for Analysing Cryptographic Protocols Using Non-Interference. 
    A.Durante, R.Focardi, R.Gorrieri. 
    ACM Transactions on Software Engineering and Methodology (TOSEM) volume 9(4), pages 489-530, October 2000. 

    A Formalization of Credit and Responsibility Within the GNDC Schema. 
    Roberto Gorrieri, Fabio Martinelli, Marinella Petrocchi. 
    In procs. First International Workshop on Security and Trust Management (STM'05) 
    Electr. Notes Theor. Comput. Sci. 157(3): 61-78 (2006). 

    Towards a Formal Treatment of Secrecy Against Computational Adversaries. 
    Angelo Troina, Alessandro Aldini, Roberto Gorrieri. 
    Global Computing 2004, LNCS 3267, pages 77-92, 2004. 

    Approximating Imperfect Cryptography in a Formal Model 
    A.Troina, A.Aldini, R. Gorrieri  
    In procs. workshop finale del progetto MEFISTO, ENTCS 99:183-203, 2004. 

    Process Algebraic Frameworks for the Specification and Analysis of Cryptographic Protocols 
    R.Gorrieri, F.Martinelli. 
    In procs. 28th International Symposium on Mathematical Foundations of Computer Science (MFCS03) 
    LNCS 2747, 46-67, Springer, Bratislava (SK), August 2003. 

    Classification of Security Properties. Part II: Network Security 
    R.Focardi, R.Gorrieri, F.Martinelli. 
    In "Foundations of Security Analysis and Design II", LNCS 2946, 139-185, Springer, 2004. 

    Formal analysis of some timed security properties in wireless protocols 
    R.Gorrieri, F.Martinelli, M.Petrocchi, A.Vaccarelli. 
    In procs. Sixth IFIP Workshop on Formal Methods for Open Object-based Distributed Systems (FMOODS'03), LNCS 2884, 139-154, Springer, 2003. 

    Compositional Verification of Integrity for Digital Stream Signature Protocols 
    R.Gorrieri, F.Martinelli, M.Petrocchi, A.Vaccarelli. 
    In procs. Third International Conference on Application of Concurrency to System Design (ACSD'03), IEEE Press, 142-149, 2003. 

    A Probabilistic Formulation of Imperfect Cryptography 
    A.Troina, A.Aldini, R.Gorrieri. 
    In procs. Workshop on Issues in Security and Petri Nets (WISP), Technical Report of the University of Eindhoven, June 2003. 

    A Simple Language for Real-time Cryptographic Protocol Analysis 
    R.Gorrieri, E.Locatelli, F.Martinelli. 
    In procs. European Symposium on Programming (ESOP'03), LNCS 2618, 114-128, Springer, 2003. 

    Security Analysis of a Probabilistic Non-repudiation Protocol 
    A.Aldini, R.~Gorrieri. 
    In procs. 10th Int.l Workshop on Process Algebras and Performance Modeling (PAPM '02)}, LNCS 2399, 17-36, 2002. 

    CVS at Work: A Report on new Failures upon some Cryptographic Protocols 
    A.Durante, R.Focardi, R.Gorrieri. 
    In procs. Int.l Workshop Mathematical Methods, Models and Architectures for Computer Networks Security, 
    LNCS 2052, 287-299, Springer, 2001. 

    Message Authentication through Non Interference 
    R.Focardi, R.Gorrieri, F.Martinelli.  
    In procs. Eighth Int.l Conference on Algebraic Methodology and Software Technology (AMAST'00) 
    LNCS 1816, Springer, pages 258-272, 2000. 

    Non interference for the analysis of cryptographic protocols 
    R.Focardi, R.Gorrieri, F.Martinelli. 
    In procs. International Colloquium on Automata, Languages and Programming (ICALP'00) 
    (U.Montanari, E.Welzl eds.), LNCS 1853, 354-372, Springer, July 2000. 

    Secrecy in Security Protocols as Non Interference 
    R.Focardi, R.Gorrieri, F.Martinelli. 
    In procs. DERA/RHBNC Workshops on Secure Architectures and Information Flow, EENTCS 32, 2000. 

    CVS: A Compiler for the Analysis of Cryptographic Protocols. 
    A.Durante, R.Focardi, R.Gorrieri, Procs of IEEE CSFW 12, 203-212, 1999. 

    Using Non Interference for the Analysis of Security Protocols. 
    Riccardo Focardi, Anna Ghelli and Roberto Gorrieri. 
    In Proceedings of DIMACS Workshop on Design and Formal Verification of Security Protocols (H. Orman and C. Meadows Ed.) 
    September 3-5, 1997, DIMACS Center, CoRE Building, Rutgers University. 


    Back to Top

    Applications 

    On Securing Real-time Speech Transmission over the Internet: an Experimental Study. 
    A.Aldini, M.Roccetti, R. Gorrieri. 
    EURASIP Journal on Applied Signal Processing, volume 10:1027-1042, 2003. 

    Coping with Denial of Service due to Malicious Java Applets. 
    M.F.Florio, R.Gorrieri, G.Marchetti. 
    Computer Communications 23(17):1645-1654, 2000. 

    Security Issues in the Tuple-Space Coordination Model. 
    Mario Bravetti, Nadia Busi, Roberto Gorrieri, Roberto Lucchi, Gianluigi Zavattaro. 
    In procs. Second IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust (FAST'04), Springer, pages 1-12, 2004. 

    Contrasting Malicious Java Applets by Modifying the Java Virtual Machine. 
    Vincenzo Ciaschini, Roberto Gorrieri. 
    In procs. 19th Int.l Information Security Conference (SEC'04), Kluwer, pages 47-64, 2004. 

    Combining partitions in SecSpaces 
    M. Bravetti, R. Gorrieri, R. Lucchi, G. Zavattaro. 
    in Proc. of the Mefisto (formal methods for security and time) project final workshop 
    ENTCS 99:31-47, Pisa (Italy), November 2003. 

    A Formal Approach for Checking Security Properties in SecSpaces 
    M.Bravetti, R.Gorrieri, R.Lucchi. 
    In procs. Workshop on Security Issues in Corrdination Models, Languages and Systems (SecCo), ENTCS 85.3, 2003. 

    A Study about Trade-off between Performance and Security in an Internet Audio Mechanism 
    A. Aldini, R. Gorrieri. 
    In Global Computing: Programming Environments, Languages, Security and Analysis of Systems 
    LNCS 2874, Springer, 203-228, 2003. 

    An Adaptive Mechanism for Real-time Secure Speech Transmission over the Internet 
    A.Aldini, R.Gorrieri, M.Roccetti. 
    In Proc. of 2nd IP-Telephony Workshop (IP-Tel2001), pages 64-72, Columbia University, New York, April 2001. 

    Applet Watch-Dog: A Monitor for Controling the Execution of Java Applets. 
    R. Gorrieri and G. Marchetti. 
    In Proc. of Fourteenth IFIP International Information Security Conference (SEC'98), G. Papp and R.Posch eds., September 1998. 


    Back to Top

    Timed and Real-time Models 

    Performance Preorder and Competitive Equivalence. 
    F.Corradini, R. Gorrieri e M. Roccetti. 
    Acta Informatica, volume 34 (11), 805-835, 1997. 

    A Theory of Processes with Durational Actions. 
    R. Gorrieri, M. Roccetti and E. Stancampiano. 
    Theoretical Computer Science, volume 140(1):73-94, 1995. 

    A Study on the Specification and Verification of Performance Properties. 
    X.J. Chen, F. Corradini e  R. Gorrieri. 
    In Proc. of Sixth International Conference on Algebraic Methodology and Software Technology (AMAST'96), 
    M. Wirsing ed., LNCS 1101, Springer-Verlag, pag. 306-320, Monaco di Baviera (Germany), July 1996. 

    Performance Preorder: Ordering Processes with respect to Speed. 
    F.Corradini, R. Gorrieri and M. Roccetti. 
    In Proc. of twentyth International Symposium on Mathematical Foundations of Computer Science (MFCS'95), 
    P. Hajek and J. Wiedermann eds., LNCS 969, Springer-Verlag, pag. 444-453, Praga (Cechia), August 1995. 

    Real-Time System Verification using P/T Nets. 
    R. Gorrieri and G. Siliprandi. 
    In Proc. of Computer Aided Verification (CAV'94), 
    D.L. Dill ed., LNCS 818, Springer-Verlag, pag. 14-26, Stanford (CA), June 1994. 
     
    Towards Performance Evaluation in Process Algebras. 
    R. Gorrieri and M. Roccetti. 
    In Proc. of Third International Conference on Algebraic Methodology and Software Technology (AMAST'93), 
    M. Nivat, C. Rattray, T. Rus and G. Scollo eds., Workshops in Computing, Springer, pag. 289 - 296, Enschede (H), June 1993. 
     


    Back to Top

    Theory of Stochastic Process Algebra and Stochastic Petri Nets 

    The Theory of Interactive Generalised Semi-Markov Processes. 
    M.Bravetti, R.Gorrieri. 
    Theoretical Computer Science, volume 282(1):5-32, 2002. 

    A Formal Approach to the Integration of Performance Aspects in the Modeling and Analysis of Concurrent Systems. 
    M. Bernardo, L. Donatiello, R. Gorrieri. 
    Information and Computation,  Volume 144(2), pagine 83-154, 1998. 

    A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. 
    M. Bernardo, R. Gorrieri. 
    Theoretical Computer Science 202:1-54, 1998. 

    Corrigendum to "the paper above". 
    M.Bernardo, R.Gorrieri. 
    Theoretical Computer Science, Volume 254(1-2):691-694, 2001. 

    A Distributed Semantics for EMPA Based on Stochastic Contextual Nets. 
    M. Bernardo, N. Busi, R. Gorrieri. 
    Computer Journal 38:492-509, December 1995. 

    Stochastic Process Algebras: Past, Present and Future 
    R.Gorrieri. 
    In procs. 7th Int. Workshop on Process Algebras and Performance Modeling (PAPM '99) 
    (J. Hillston ed.), Zaragoza (Spain), September 1999. 

    Interactive Generalised Semi-Markov Processes 
    M. Bravetti, R. Gorrieri. 
    In Proc. 7th Workshop on Process Algebras and Performance Modeling (PAPM '99), 83-98, Zaragoza (Spain), September 1999. 

    Towards Performance Evaluation with General Distributions in Process Algebras. 
    M. Bravetti, M. Bernardo, R. Gorrieri. 
    In Proc. of the 9th Int. Conf. on Concurrency Theory (CONCUR '98), LNCS 1466:405-422, Nice (France), September 1998. 

    A Note on the Congruence Proof for Recursion in Markovian Bisimulation Equivalence. 
    M. Bravetti, M. Bernardo, R. Gorrieri. 
    In Proc. of the 6th Int. Workshop on Process Algebras and Performance Modelling (PAPM '98) 
    Nice (France), September 1998. 

    From EMPA to GSMPA: Allowing for General Distributions. 
    M. Bravetti, M. Bernardo, R. Gorrieri. 
    In Proc. of the 5th Int. Workshop on Process Algebras and Performance Modelling (PAPM '97), 
    E. Brinksma and A. Nymeyer editors, pp. 17-33, Enschede (The Netherlands), June 1997. 

    Extended Markovian Process Algebra. 
    M. Bernardo, R. Gorrieri. 
    In Proc. of the 7th Int. Conf. on Concurrency Theory (CONCUR '96), 
    U. Montanari and V. Sassone editors, LNCS 1119:315-330, Pisa (Italy), August 1996. 

    Giving a Net Semantics to Markovian Process Algebra. 
    M. Bernardo, L. Donatiello, R. Gorrieri. 
    Proc. of the 6th Int. Workshop on Petri Nets and Performance Models (PNPM '95), IEEE-CS Press, pp. 169-178, 
    Durham (NC), October 1995. 

    Integrated Analysis of Concurrent Distributed Systems using Markovian Process Algebra. 
    M. Bernardo, L. Donatiello, R. Gorrieri. 
    In Proc. of the 7th Int. Conf. on Formal Desc. Tech. for Distributed Systems and Communication Protocols (FORTE '94), 
    D. Hogrefe and S. Leue editors, Chapman & Hall, pp. 455-457, Berne (Switzerland), October 1994. 

    Modeling and Analyzing Concurrent Systems with MPA. 
    M. Bernardo, L. Donatiello, R. Gorrieri. 
    In Proc. of the 2nd Workshop on Process Algebras and Performance Modelling (PAPM '94), 
    U. Herzog and M. Rettelbach editors, pp. 175-189, Erlangen (Germany), July 1994. 


    Back to Top

    Applications of SPA 

    QoS Evaluation of IP telephony Services: A Specification Language Based Simulation Software Tool 
    M. Roccetti, A. Aldini, M. Bernardo, R. Gorrieri. 
    Journal of Systems Analysis, Modelling and Simulation, volume 43(12):1747-1759, December 2003. 

    Comparing the QoS of Internet Audio Mechanisms via Formal Methods. 
    A.Aldini, M.Bernardo, R.Gorrieri, M.Roccetti. 
    ACM Transactions on Modeling and Computer Simulation (TOMACS), volume 11(1):1-42, January 2001. 

    Formal Performance Modeling and Evaluation of an Adaptive Mechanism for Packetized Audio over the Internet. 
    M. Bernardo, R. Gorrieri, M. Roccetti. 
    Formal Aspects of Computing 10(4):313-337, 1998. 

    An Algebraic Model for Evaluating the Performance of an ATM Switch with Explicit Rate Marking 
    A. Aldini, M. Bernardo, R. Gorrieri. 
    In Proc. 7th Workshop on Process Algebras and Performance Modeling (PAPM '99), 119-138, Zaragoza (Spain), September 1999. 

    A Simulative Analysis of Internet Audio Mechanisms Using Formal Methods 
    A.Aldini, M.Bernardo, R.Gorrieri, M.Roccetti. 
    In procs. 11th European Simulation Symp. (ESS '99), Society for Computer Simulation Int.l, pages 281-288, 1999. 

    Packetized Audio for Industrial Applications: A Simulation Study. 
    M.Roccetti, M.Bernardo, R.Gorrieri. 
    In Proc. of 10th European Simulation Symposium and Exhibition (ESS'98), Nottingham (UK), October 1998. 

    A Stochastic Process Algebra Model for the Analysis of the Alternating Bit Protocol. 
    M. Bernardo, L. Donatiello, R. Gorrieri. 
    In Proc. of the 11th Int. Symp. on Computer and Information Sciences (ISCIS XI), 
    V. Atalay, U. Halici, K. Inan, N. Yalabik and A. Yazici editors, METU, pp. 375-384, Antalya (Turkey), November 1996. 

    Integrated Functional and Performance Analyses of Concurrent Distributed Systems Described with the Language EMPA. 
    M. Bernardo, L. Donatiello, R. Gorrieri. 
    In Proc. of the 1st Workshop on Distributed Systems: Algorithms, Architectures and Languages (WDSAAL '96), 
    A. Bertossi, M. Bonucelli and R. De Nicola editors, pp. 5-6, Levico (Italy), June 1996. 


    Back to Top