Publications

[ 2012 | 2011 | 2010 ]

2012

F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, and G. P. Rossi. Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories. In Journal of Satisfiability, Boolean Modeling, and Computation. Vol 8 (2012), pages 29-61.
F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharyagina. Lazy Abstraction with Interpolants for Arrays (extended version with proofs). In Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR18), March 10-15, Venzuela.

[ Top of the page ]

A. Armando and S. Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies. Proc. of the 7th Int. Workshop on Security and Trust Management (co-located with 5th IFIP WG 11.11 Int. Conference on Trust Management), June 27-28, Copnhagen, Denmark, 2011. To appear also in LNCS.

F. Alberti, A. Armando, and S. Ranise. ASASP: Automated Symbolic Analysis of Security Policies. Proc. of the 23rd Conference on Automated Deduction (CADE), 2011. To appear in LNCS.
C. Lynch, S. Ranise, C. Ringeissen, and D.-K. Tran. Automatic Decidability and Combinability. Information and Computation 209:7 (July, 2011) 1026-1047
R. Bruttomesso, S. Ghilardi, S. Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays, Proc. of the 22nd Int. Conf. on Rewriting Techniques and Applications (RTA '11), Leibniz Int. Proc. in Informatics, Dagstuhl Publishing, 2011 (Extended version with proofs and technical details).
M. Barletta, S. Ranise, and L. Vigano. A Declarative Two-level Framework to Specify and Verify Workflow and Authorization Policies in Service Oriented Architetures. In Journal of Service Oriented Computing and Applications, vol. 5, nr. 1, 2011.

A. Armando, R. Carbone, L. Compagna, J. Cuellar, G. Pellegrino, and A. Sorniotti. From Multiple Credentials to Browser-based Single Sign-On: Are We More Secure? In the Proceedings of the 26th IFIP TC-11 International Information Security Conference (SEC 2011), Luzern, Switzerland, June 7-9, 2011.
A. Armando, R. Carbone, L. Compagna, and G. Pellegrino. Automatic Security Analysis of SAML-based Single Sign-On Protocols. In Digital Identity and Access Management: Technologies and Frameworks. IGI Global. R. Sharman, S. Das Smith, and M. Gupta, editors. To appear.
A. Armando, E. Giunchiglia, M. Maratea, and S. E. Ponta. An Action-based Approach to the Formal Specification and Automatic Analysis of Business Processes under Authorization Constraints. To appear in the Journal of Computer and System Science (special issue on Knowledge Representation and Reasoning).
F. Alberti, A. Armando, and S. Ranise. Efficient Symbolic Automated Analysis of Administrative Role Based Access Control Policies. In Proc. of the 6th ACM Symposium on Information, Computer, and Communications Security (ASIACCS), Hong Kong, March 22-24, 2011. To appear in ACM SIG, 2011 [Tool and benchmarks used in the paper].

[ Top of the page ]

S. Ghilardi and S. Ranise. Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. In Logical Methods in Computer Science (LMCS), Vol. 6, Issue 4, 2010.
A. Armando and S. Ranise. Automated Symbolic Analysis of ARBAC Policies. In Proc. of 6th Int. Workshop on Security and Trust Management (co-located with EUROPKI'10, CRITIS'10, and ESORICS'10), Athens, Sept. 23-24 (2010). To appear in LNCS, Springer, 2010. (Extended version).
A. Merlo and A. Armando. Cooperative Access Control for the Grid. Proceedings of the 6th International Conference on Information Assurance and Security (IAS 2010), Atlanta, GA, USA, August 23-24, 2010.

M. Barletta, A. Calvi, S. Ranise, L. Vigano, and L. Zanetti. WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications. In Proc. of 1st Workshop on Software Service (satellite of SYNASC symposium), Timisoara, Sept. 23-25 (2010). To appear in IEEE Comp. Society, 2010.
A. Calvi, S. Ranise, L. Vigano. Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC. In Proc. of 1st Workshop on Software Service (satellite of SYNASC symposium), Timisoara, Sept. 23-25 (2010). To appear in IEEE Comp. Society, 2010.
A. Carioni, S. Ghilardi, S. Ranise. MCMT in the Land of Parameterized Timed Automata, In Proc. of VERIFY Workshop, co-located with IJCAR, Edinburgh (2010)
S. Ghilardi and S. Ranise. MCMT: a Model Checker Modulo Theories (system description), Proc. of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Springer LNAI, vol. 6173, pp. 22-29.

[ Top of the page ]