Publications

[1] Humberto Abdelnur, Tigran Avanesov, Michaël Rusinowitch, and Radu State. Abusing SIP Authentication. In Massimiliano Rak, Ajith Abraham, and Valentina Casola, editors, Proceedings of the Fourth International Symposium on Information Assurance and Security (ISIAS’08), pages 237-242. IEEE Computer Society Press, 2008. [ pdf ]
[2] Humberto Abdelnur, Tigran Avanesov, Michael Rusinowitch, and Radu State. Abusing SIP authentication. Journal of Information Assurance and Security, 4(4):311-318, 2009. [ pdf ]
[3] Zeeshan Ahmed, Abdessamad Imine, and Michael Rusinowitch. Safe and Efficient Strategies for Updating Firewall Policies. In Sokratis K. Katsikas, Javier Lopez, and Miguel Soriano, editors, 7th International Conference on Trust, Privacy & Security in Digital Business (TrustBus 2010), volume 6264 of Lecture Notes of Computer Science, pages 45-57, Bilbao, Spain, 08 2010. Springer. [ pdf ]
[4] Francesco Alberti, Alessandro Armando, and Silvio Ranise. Efficient Symbolic Automated Analysis of Administrative Role Based Access Control Policies. In Proceedings of the 6th ACM Symposium on Information, Computer, and Communications Security (ASIACCS), Hong Kong, March 22-24, 2011. ACM SIG, to appear. [ pdf ]
[5] Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michaël Rusinowitch. Unification modulo homomorphic encryption. In Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings, volume 5749 of Lecture Notes in Computer Science. Springer, 2009. [ pdf ]
[6] Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michael Rusinowitch. Cap unification: Application to protocol security modulo homomorphic encryption. In 5th ACM Symposium on Information, Computer and Communications Security – ASIACCS 2010, Beijing, China, April 2010. ACM. [ pdf ]
[7] Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michael Rusinowitch. Unification modulo Homomorphic Encryption. Journal of Automated Reasoning, to appear.
[8] Alessandro Armando, Roberto Carbone, and Luca Compagna. LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics, special issue on “Logic and Information Security”, 2009. [ pdf ]
[9] Alessandro Armando, Roberto Carbone, Luca Compagna, Jorge Cuellar, and Llanos Tobarra Abad. Formal analysis of saml 2.0 web browser single sign-on: Breaking the saml-based single sign-on for google apps. In Vitaly Shmatikov, editor, Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), pages 1-10. ACM Press, 2008. [ pdf ]
[10] Alessandro Armando, Roberto Carbone, Luca Compagna, Jorge Cuéllar, Giancarlo Pellegrino, and Alessandro Sorniotti. From Multiple Credentials to Browser-based Single Sign-On: Are We More Secure? In Proceedings of IFIP SEC 2011, to appear.
[11] Alessandro Armando, Roberto Carbone, Luca Compagna, Keqin Li, and Giancarlo Pellegrino. Model-Checking Driven Security Testing of Web-Based Applications. In Proceedings of the 2010 Third International Conference on Software Testing, Verification, and Validation Workshops, ICSTW’10, pages 361-370. IEEE Computer Society, 2010.[ pdf ]
[12] Alessandro Armando, Luca Compagna, Roberto Carbone, and Giancarlo Pellegrino. Automatic Security Analysis of SAML-based Single Sign-On Protocols. In Raj Sharman and Sanjukta Das Smith and Manish Gupta, editor, Digital Identity and Access Management: Technologies and Frameworks. IGI Global, 2010. [ pdf ]
[13] Alessandro Armando, Enrico Giunchiglia, Marco Maratea, and Serena Elisa Ponta. An action-based approach to the formal specification and automated analysis of business processes under authorization constraints. Journal of Computer and Systems Sciences: Special issue on Knowledge Representation and Reasoning, to appear. [ pdf ]
[14] Alessandro Armando, Enrico Giunchiglia, and Serena Elisa Ponta. Formal specification and automatic analysis of business processes under authorization constraints: An action-based approach. In Guenther Pernul, Simone Fischer-Huebner, and Costas Lambrinoudakis, editors, TrustBus’09: Proceedings of the 6th International Conference on Trust, Privacy and Security in Digital Business, pages 63-72, Berlin, Heidelberg, 2009. Springer-Verlag. [ pdf ]
[15] Alessandro Armando and Serena Elisa Ponta. Model checking of security-sensitive business processes. In Pierpaolo Degano and Joshua Guttman, editors, Formal Aspects in Security and Trust: 6th International Workshop, FAST 2009, Eindhoven, The Netherlands, November 5-6, 2009, Revised Selected Papers, volume 5983 of Lecture Notes in Computer Science, pages 66-80. Springer, 2010. [ pdf ]
[16] Alessandro Armando and Silvio Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proceedings of the 6th International Workshop on Security and Trust Management STM’10 (co-located with EUROPKI’10, CRITIS’10, and ESORICS’10), Athens, September 23-24, 2010, To appear in Lecture Notes in Computer Science. [ pdf ]
[17] Charu Arora and Mathieu Turuani. Validating Integrity for the Ephemer- izer’s Protocol with CL-Atse. In Formal to Practical Security: Papers Issued from the 2005-2008 French-Japanese Collaboration, pages 21–32. Springer, 2009. [ pdf ]
[18] Wihem Arsac, Giampaolo Bella, Xavier Chantry, and Luca Compagna. Validating Security Protocols under the General Attacker. In Pierpaolo Degano and Luca Viganò, editors, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS 2009), ENTCS. Elsevier-Science, 2009.
[19] Wihem Arsac, Giampaolo Bella, Xavier Chantry, and Luca Compagna. Multi-attacker protocol validation. Journal of Automated Reasoning, pages 1-36, 2010. 10.1007/s10817-010-9185-y.
[20] Wihem Arsac, Giampaolo Bella, Xavier Chantry, and Luca Compagna. Attacking Each Other. In Bruce Christianson, Bruno Crispo, James A. Malcolm, and Michael Roe, editors, 17th International Workshop on Security Protocols (IWSP 2009), Cambridge, UK, April 1-3, 2009, Lecture Notes in Computer Science. Springer, to appear.
[21] Wihem Arsac, Luca Compagna, Giancarlo Pellegrino, and Serena Elisa Ponta. Security Validation of Business Processes via Model-checking. In International Symposium on Engineering Secure Software and Systems (ESSoS 2011). Lecture Notes in Computer Science, Springer-Verlag, to appear. [ pdf ]
[22] Tigran Avanesov, Yannick Chevalier, Michael Rusinowitch, and Mathieu Turuani. Satisfiability of general intruder constraints with a set constructor. In José M. Fernandez, editor, The Fifth International Conference on Risks and Security of Internet and Systems – CRiSIS 2010, Montreal, Canada, October 10-13, 2010. IEEE XPlore, 2010. [ pdf ]
[23] Bahareh Badban and Mohammad Torabi Dashti. Semi-linear Parikh images of regular expressions via reduction. In Proceedings of the 35th international symposium on Mathematical Foundations of Computer Science (MFCS’10), Brno, Czech Republic, August 2010, volume 6281 of Lecture Notes in Computer Science, pages 653-664. Springer, 2010. [ pdf ]
[24] Philippe Balbiani, Fahima Cheikh, and Guillaume Feuillade. Considérations relatives à la décidabilité et à la complexité du problème de la composition de services. In Proceedings of the Journées Francophones Modèles formels de l’Interaction (MFI 2007), pages 261-268, Paris, France, 2007. Annales du LAMSADE.
[25] Philippe Balbiani, Fahima Cheikh, and Guillaume Feuillade. Composition of interactive web services based on controller synthesis. In Jyothishman Pathak, Samik Basu, Marco Pistore, Prashant Doshi, and Rama Akkiraju, editors, Proceedings of the 2008 IEEE Congress on Services – Part I, SERVICES’08, pages 521-528, Washington, DC, USA, 2008. IEEE Computer Society. [ pdf ]
[26] Philippe Balbiani, Fahima Cheikh, and Guillaume Feuillade. Composition of Web services: algorithms and complexity. Presented at the first Interaction and Concurrency Experience Workshop, sponsored by the ESF and co-located with ICALP’08, 2008.
[27] Philippe Balbiani, Fahima Cheikh, and Guillaume Feuillade. Résultats de complexité pour le problème de la composition d’agents. Cinquièmes Journées Francophones Modèles Formels de l’Interaction (MFI 09), to appear, 2009.
[28] Philippe Balbiani, Fahima Cheikh, and Guillaume Feuillade. Controller/orchestrator synthesis via filtration. Electronic Notes in Theoretical Computer Science, 262:33-48, 2010.
[29] Philippe Balbiani, Fahima Cheikh Alili, Pierre-Cyril Héam, and Olga Kouchnarenko. Composition of services with constraints. Electronic Notes in Theoretical Computer Science, 263:31-46, June 2010.
[30] Philippe Balbiani, Yannick Chevalier, and Marwa El Houri. A Logical Approach to Dynamic Role-Based Access Control. In Artificial Intelligence: Methodology, Systems, and Applications, 13th International Conference, AIMSA 2008, volume 5253 of Lecture Notes in Computer Science, pages 194-208. Springer, 2008. [ pdf ]
[31] Philippe Balbiani, Yannick Chevalier, and Marwa El Houri. Approche logique pour les contraintes de contrôle d’accès dans les services web. Presented at the Inforsid/SDEC 2009 workshop, 2009.
[32] Philippe Balbiani, Yannick Chevalier, and Marwa El Houri. A logical framework for reasoning about policies with trust negotiations and workflows in a distributed environment. In The fourth International Conference on Risks and Security of Internet and Systems – CRiSIS 2009, Toulouse, France, October 19-22, 2009. IEEE XPlore, 2009.
[33] Philippe Balbiani, Yannick Chevalier, and Marwa El Houri. An intruder model for trust negotiation. In José M. Fernandez, editor, The Fifth International Conference on Risks and Security of Internet and Systems – CRiSIS 2010, Montreal, Canada, October 10-13, 2010. IEEE XPlore, 2010.
[34] Michele Barletta, Alberto Calvi, Silvio Ranise, Luca Viganò, and Luca Zanetti. WSSMT: towards the automated analysis of Security-Sensitive Services and Applications. In Proceedings of Synasc’10. IEEE Computer Society Press, to appear. [ pdf ]
[35] Michele Barletta, Silvio Ranise, and Luca Viganò. Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures. In Proceedings of the 2009 International Symposium on Secure Computing (SecureCom 2009), Volume 3 of 2009 International Conference on Computational Science and Engineering (CSE 2009), pages 289-299. IEEE Computer Society Press, 2009. http://doi.ieeecomputersociety.org/10.1109/CSE.2009.172. [ pdf full version ] [ pdf ]
[36] Michele Barletta, Silvio Ranise, and Luca Viganò. A Declarative Two-Level Framework to Specify and Verify Workflow and Authorization Policies in Service-Oriented Architectures. Service-Oriented Computing and Applications, 2010, DOI 10.1007/s11761-010-0073-4.
[37] David Basin, Carlos Caleiro, Jaime Ramos, and Luca Viganò. A Labeled Tableaux System for the Distributed Temporal Logic DTL. In Stéphane Demri and Christian S. Jensen, editors, Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME 2008), pages 101-109. IEEE Computer Society Press, Los Alamitos, CA, 2008. [ pdf ]
[38] David Basin and Cas Cremers. Degrees of security: Protocol guarantees in the face of compromising adversaries. In A. Dawar and H. Veith, editors, CSL 2010: Proceedings of the 19th EACSL Annual Conference on Computer Science Logic, volume 6247 of Lecture Notes in Computer Science, pages 1-18. Springer, 2010. [ pdf ]
[39] David Basin and Cas Cremers. Modeling and analyzing security in the presence of compromising adversaries. In D. Gritzalis, B. Preneel, and M. Theoharidou, editors, Computer Security – ESORICS 2010, volume 6345 of Lecture Notes in Computer Science, pages 340-356. Springer, 2010. [ pdf ]
[40] Giampaolo Bella and Luca Compagna. Special track on computer security 2009: editorial message. In Roger L. Wainwright and Hisham Haddad, editors, SAC’08: Proceedings of the 2008 ACM Symposium on Applied Computing, Fortaleza, Ceara, Brazil, March 16-20, 2008. ACM, 2008.
[41] Giampaolo Bella and Luca Compagna. Special track on computer security 2009: editorial message. In SAC’09: Proceedings of the 2009 ACM symposium on Applied Computing, Honolulu, Hawaii, USA, March 08-12, 2008. ACM, 2009.
[42] Giampaolo Bella, Francesco Librizzi, and Salvatore Riccobene. A privacy paradigm that tradeoffs anonymity and trust. In Proceedings of the 2008 International Conference on Software, Telecommunications and Computer Networks – SoftCOM 2008. IEEE Computer Society, 2008. [ pdf ]
[43] Giampaolo Bella, Francesco Librizzi, and Salvatore Riccobene. Realistic threats to self-enforcing privacy. In Proceedings of the 4th International Symposium on Information Assurance and Security, pages 155-160. IEEE Computer Society, 2008. [ pdf ]
[44] Davide Benetti, Massimo Merro, and Luca Viganò. Model Checking Ad Hoc Network Routing Protocols: ARAN vs. endairA. In Proceedings of eighth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, September 14-18, 2010, pages 191-202. IEEE Computer Society Press, 2010. [ pdf ]
[45] Daniele Berardi, Fahima Cheikh, Giuseppe DeGiacomo, and Fabio Patrizi. Automatic service composition via simulation. International Journal of Foundations of Computer Science, 19(2):429-451, 2008.
[46] Achim D. Brucker and Sebastian A. Mödersheim. Integrating automated and interactive protocol verification. In Pierpaolo Degano and Joshua Guttman, editors, Formal Aspects in Security and Trust: 6th International Workshop, FAST 2009, Eindhoven, The Netherlands, November 5-6, 2009, Revised Selected Papers, volume 5983 of Lecture Notes in Computer Science, pages 248-262. Springer, 2010. [ pdf ]
[47] Elisa Burato, Matteo Cristani, and Luca Viganò. A Deduction System for Meaning Negotiation. In Postproceedings of DALT’10. Springer,to appear. [ pdf ]
[48] Alberto Calvi, Silvio Ranise, and Luca Viganò. Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC. In Proceedings of WoSS’10. IEEE Computer Society Press, to appear. [ pdf ]
[49] Jan Camenisch, Sebastian Mödersheim, Gregory Neven, Franz-Stefan Preiss, and Dieter Sommer. A card requirements language enabling privacy-preserving access control. In ACM Symposium on Access Control Models and Technologies (SACMAT). ACM, 2010. [ pdf ]
[50] Jan Camenisch, Sebastian Alexander Mödersheim, and Dieter Sommer. A formal model of Identity Mixer. In Proceedings of the 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), pages 198-214. Springer, 2010. [ pdf ]
[51] Roberto Carbone. LTL Model-Checking for Security Protocols. AI Commun., to appear. [ pdf ]
 [52] Roberto Carbone. LTL Model-Checking for Security Protocols. PhD thesis, Università degli Studi di Genova, Italy, 2009.
[53] Jan Cederquist and Mohammad Torabi Dashti. Complexity of Fairness Constraints for the Dolev-Yao Attacker Model. Proceedings of ACM SAC 2011, 26th Symposium On Applied Computing, Taichung, Taiwan, March 21–24, 2011, to appear. [ pdf ]
[54] Fahima Cheikh. Composition de services: algorithmes et complexité. PhD thesis, Universitè de Toulouse, Toulouse, France, 2009.
[55] Yannick Chevalier. Finitary deduction systems. Presented at the 2010 Security and Rewriting (Secret) workshop, 2010.
[56] Yannick Chevalier and Mounira Kourjieh. New decidability result for ground entailment problems and application to security protocols. In Dov M. Gabbay and Leendert van der Torre, editors, Proceedings of the workshop on Logics in Security, organised as part of the European Summer School on Logic, Language and Information (ESSLLI), Copenhagen, Denmark, August 2010. 2010.
[57] Yannick Chevalier, Mohamed Anis Mekki, and Michaël Rusinowitch. Orchestration under security constraints. Presented at the Formal Aspects of Security and Trust, FAST’09 workshop, 2009. [ pdf ]
[58] Yannick Chevalier, Mohammed Anis Mekki, and Michael Rusinowitch. Automatic Composition of Services with Security Policies. In Web Service Composition and Adaptation Workshop (held in conjunction with SCC/SERVICES-2008), pages 529-537. IEEE Computer Society Press, 2008. [ pdf ]
[59] Yannick Chevalier and Michael Rusinowitch. Compiling and securing cryptographic protocols. Information Processing Letters, 110(3):116-122, 2010.
[60] Yannick Chevalier and Michael Rusinowitch. Decidability of Equivalence of Symbolic Derivations. Journal of Automated Reasoning, 2010. 10.1007/s10817-010-9199-5.
[61] Yannick Chevalier and Michael Rusinowitch. Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures. Theoretical Computer Science, 411(10):1261-1282, 2010. [ pdf ]
[62] Najah Chridi. Contributions à la vérification automatique de protocoles de groupes. PhD thesis, Universit Henri Poincaré – Nancy 1, September 2009. [ pdf ]
[63] Najah Chridi, Mathieu Turuani, and Michael Rusinowitch. Towards a Constrained-based Verification of Parameterized Cryptographic Protocols. In Michael Hanus, editor, Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, volume 5438 of Lecture Notes in Computer Science. Springer, 2008. [ pdf ]
[64] Najah Chridi, Mathieu Turuani, and Mohammad Rusinowitch. Decidable analysis for a class of cryptographic group protocols with unbounded lists. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF’09), pages 277-289. IEEE Computer Society, 2009. [ pdf ]
[65] Luca Compagna, Ulrich Flegel, and Volkmar Lotz. Towards Validating Security Protocol Deployment in the Wild. In Computer Software and Applications Conference, 2009. COMPSAC ’09. 33rd Annual IEEE International, Seattle, WA, USA, July 20-24, 2009. IEEE Computer Society Press, 2009.
[66] Matteo Cristani, Erisa Karafili, and Luca Viganò. Blocking underhand attacks by hidden coalitions. In Proceedings of ICAART 2011: 3rd International Conference on Agents and Artificial Intelligence (ICAART), Rome, Italy, January 28-30, 2011. SciTePress, to appear. [ pdf ]
[67] Wan Fokkink, Mohammad Torabi Dashti, and Anton Wijs. Partial order reduction for branching security protocols. In Application of Concurrency to System Design (ACSD), 2010 10th International Conference on, Braga, Portugal, June 21-25, 2010, pages 191-200. IEEE Computer Society, 2010. [ pdf ]
[68] Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, and Daniele Zucchelli. Towards smt model checking of array-based systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Proceedings of the 6th International Workshop on Satisfiability Modulo Theories (SMT’08), in Proceedings of the 4th international joint conference on Automated Reasoning, pages 67-82. Springer, 2008. [ pdf ]
[69] Silvio Ghilardi, Silvio Ranise, and Thomas Valsecchi. Light-weight smt-based model checking. Electronic Notes in Theoretical Computer Science, 250:85-102, September 2009. [ pdf ]
[70] Bogdan Groza and Marius Minea. A calculus to detect guessing attacks. In Pierangela Samarati, Moti Yung, Fabio Martinelli, and Claudio Ardagna, editors, Information Security, Proceedings of the 12th International Conference on, volume 5735 of Lecture Notes in Computer Science, pages 59-67. Springer, 2009. [ pdf ]
[71] Bogdan Groza and Marius Minea. A formal approach for automated reasoning about off-line and undetectable on-line guessing (short paper). In R. Sion, editor, Financial Cryptography and Data Security, Proceedings of the 14th International Conference on, volume 6052 of Lecture Notes in Computer Science, pages 391-399. Springer, 2010. [ pdf ]
[72] Bogdan Groza and Marius Minea. Formal modelling and automatic detection of resource exhaustion attacks. In Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS), to appear. [ pdf ]
[73] Peter Hartmann, Monika Maidl, David von Oheimb, and Richard Robinson. A case study in decentralized, dynamic, policy-based, authorization and trust management – automated software distribution for airplanes. In Jorge Cuellar and Javier Lopez, editors, Proceedings of the 6th International Workshop on Security and Trust Management STM’10 (co-located with EUROPKI’10, CRITIS’10, and ESORICS’10), Athens, September 23-24, 2010. Springer, to appear. [ pdf ]
[74] Casandra Holotescu. Black-box composition: a dynamic approach. In 9th International Workshop on Specification and Verification of Component- Based Systems SAVCBS’10, Workshop at FSE-18, Santa-Fe, New Mexico, USA, November 12, 2010, to appear. [ pdf ]
[75] Casandra Holotescu. Controlling the unknown. In Preproceedings of the First International Conference on Formal Verification of Object-Oriented Software, FoVeOOSS 2010, Paris, France, June 28–30., 2010.
[ pdf ]
[76] Casandra Holotescu. Error-avoiding adaptors for black-box software com- ponents. In 25th IEEE/ACM International Conference on Automated Software Engineering, Doctoral Symposium, Antwerp, Belgium, September 21, 2010,pages 487–492, 2010. [ pdf ]
[77] Abdessamad Imine, Asma Cherif, and Michael Rusinowitch. A Flexible Access Control Model for Distributed Collaborative Editors. In Secure Data Management, 6th VLDB Workshop, SDM 2009, volume 5776 of Lecture Notes in Computer Science, pages 89-106, Lyon, France, 2009. Springer. [ pdf ]
[78] Florent Jacquemard and Michael Rusinowitch. Closure of Hedge-Automata Languages by Hedge Rewriting. In A. Voronkov, editor, 19th International Conference on Rewriting Techniques and Applications – RTA 2008, volume 5117 of Lecture Notes in Computer Science, pages 157-171. Springer, 2008. [ pdf ]
[79] Florent Jacquemard and Michael Rusinowitch. Rewrite-based verification of XML updates. In Temur Kutsia, Wolfgang Schreiner, and Maribel Fernández, editors, 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming – PPDP’10, pages 119-130, Hagenberg, Austria, July 2010. ACM. [ pdf ]
[80] Francis Klay and Laurent Vigneron. Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder. In P. Degano, J. Guttman, and F. Martinelli, editors, 5th International Workshop on Formal Aspects in Security and Trust (FAST), volume 5491 of Lecture Notes in Computer Science, pages 165-180, Malaga, Spain, 2008. Springer. [ pdf ]
 [81] Mounira Kourjieh. Logical analysis and verification of cryptographic protocols. PhD thesis, Université de Toulouse, France, 2009.
[82] Keqin Li. Towards security vulnerability detection by source code model checking. In ICSTW’10: Software Testing, Verification, and Validation Workshops (ICSTW), 2010 Third International Conference on, Paris, France, April 6-10, 2010, pages 381-387. IEEE Computer Society, 2010. [ pdf ]
[83] Jing Liu and Laurent Vigneron. Design and Verification of a Non-Repudiation Protocol Based on Receiver-Side Smart Card. IET Information Security, 4(1):15-29, March 2010.
[84] Monika Maidl, David von Oheimb, Peter Hartmann, and Richard Robinson. Formal security analysis of electronic software distribution systems. In Michael Harrison and Mark-Alexander Sujan, editors, Proceedings of the 27th International Conference on Computer Safety, Reliability and Security (SAFECOMP), volume 5219 of Lecture Notes in Computer Science, pages 415-428. Springer, 2008. [ pdf ]
[85] Andrea Masini, Luca Viganò, and Marco Volpe. A Labeled Natural Deduction System for a Fragment of CTL*. In Sergei Artemov and Anil Nerode, editors, Proceedings of the 2009 International Symposium on Logical Foundations of Computer Science (LFCS’09), volume 5407 of Lecture Notes in Computer Science, pages 338-353. Springer, Berlin, Heidelberg, 2009. [ pdf ]
[86] Andrea Masini, Luca Viganò, and Marco Volpe. Labeled Natural Deduction for a Bundled Branching Temporal Logic. Journal of Logic and Computation, 2010, 10.1093/logcom/exq028.
[87] Sjouke Mauw, Sasa Radomirović, and Mohammad Torabi Dashti. Minimal message complexity of asynchronous multi-party contract signing. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF’09), pages 13-25. IEEE Computer Society, 2009. [ pdf ]
[88] Sebastian Mödersheim. Algebraic Properties in Alice and Bob Notation. In Availability, Reliability and Security, 2009. ARES ’09. International Conference on, Fukuoka, Japan, March 16-19, 2009. IEEE Computer Society Press, 2009. [ pdf extended version ][ pdf ]
[89] Sebastian Mödersheim and Luca Viganò. Secure Pseudonymous Channels. In Michael Backes and Peng Ning, editors, Computer Security – ESORICS 2009 (Proceedings), volume 5789 of Lecture Notes in Computer Science, pages 337-354. Springer, 2009. [ pdf ]
[90] Sebastian Mödersheim and Luca Viganò. The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols. In Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri, editors, FOSAD 2008/2009, Lecture Notes in Computer Science 5705, pages 166-194. Springer-Verlag, 2009. [ pdf ]
[91] Sebastian Mödersheim, Luca Viganò, and David Basin. Constraint Differentiation: Search-Space Reduction for the Constraint-Based Analysis of Security Protocols. Journal of Computer Security (JCS), 18(4):575-618, 2010.
[92] Sebastian Alexander Mödersheim. Abstraction by Set-Membership : Verifying Security Protocols and Web Services with Databases. In Proceedings of the 17th ACM conference on Computer and communications security, Chicago, Illinois, USA, CCS ’10, pages 351-360. ACM, 2010. [ pdf ]
[93] Simona Orzan and Mohammad Torabi Dashti. Fair exchange is incomparable to consensus. In John S. Fitzgerald, Anne Elisabeth Haxthausen, and Hüsnü Yenigün, editors, Theoretical Aspects of Computing – ICTAC 2008, Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing, volume 5160 of Lecture Notes in Computer Science, pages 349-363. Springer, 2008. [ pdf ]
[94] Carsten Rudolph, Luca Compagna, Roberto Carbone, Antonio Muñoz, and Juergen Repp. Verification of S&D Solutions for Network Communications and Devices. In George Spanoudakis, Antonio Maña Gomez, and Spyros Kokolakis, editors, Security and Dependability for Ambient Intelligence, volume 45 of Advances in Information Security, pages 143-164. Springer, 2009.
 [95] Silvio Ranise. Towards Verification of Security-Aware E-services. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, First-order Theorem Proving, FTP 2009: International Workshop on First-Order Theorem Proving proceedings, University Oslo/Departmant of Informatics: Research Report 386. University of Oslo/Department of Informatics, 2009. [ pdf ]
[96] Mohammad Torabi Dashti. Efficiency of optimistic fair exchange using trusted devices. To appear in ACM Transactions on Autonomous and Adaptive Systems. [ pdf ]
[97] Mohammad Torabi Dashti. Optimistic fair exchange using trusted devices. In Guerraoui R. and F. Petit, editors, Proceedings of the 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’09), volume 5873 of Lecture Notes in Computer Science, pages 711-725. Springer, 2009. [ pdf ]
[98] Mohammad Torabi Dashti and Sjouke Mauw. Handbook of Financial Cryptography and Security (G. Rosenberg, ed.), chapter Fair Exchange, pages 109-132. Chapmand and Hall/CRC, 2010.
[99] David von Oheimb, Monika Maidl, and Richard Robinson. Security architecture and formal analysis of an airplane software distribution system. In 26th Congress of the International Council of the Aeronautical Sciences (ICAS), pages 1-12. Proceedings on CD-ROM available from secr.exec@icas.org, 2008. http://ddvo.net/papers/ICAS08.html. [ pdf ]
[100] Bogdan Groza, Marius Minea. Customizing protocol specifications for detecting resource exhaustion and guessing attacks. In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects. Springer Verlag, 2010 (to appear) [ pdf ]
 [101] David von Oheimb and Sebastian Mödersheim. ASLan++ — A formal security specification language for distributed systems. In B. Aichernig, F. de Boer, and M. Bonsangue, editors,Formal Methods for Components and Objects, FMCO 2010, Graz, Austria,Springer LNCS, Dec. 2010. [ pdf ]