Labelled Non-Classical Logics
Kluwer Academic Publishers, 2000.
Publications
| Luca Viganò. Labelled Non-Classical Logics Kluwer Academic Publishers, 2000. |
Last modified: Sat Jan 13 12:00:11 CET 2007
Journal Papers
On the Mosaic Method for Many-Dimensional Modal Logics: A Case Study Combining Tense and Modal Operators.
Logica Universalis, to appear.
Labeled Natural Deduction for a Bundled Branching Temporal
Logic.
Journal of Logic and Computation 21:1093-1163, 2011.
Workflow and Access Control Reloaded: a Declarative Specification Framework for the Automated Analysis of Web Services.
Scalable Computing: Practice and Experience 12(1):1-20, 2011.
Distributed Temporal Logic for the Analysis of Security
Protocol Models.
Theoretical Computer Science 412(31):4007-4043, 2011.
Modal Deduction Systems for Quantum State Transformations.
Journal of Multiple-Valued Logic and Soft Computing
17(5-6):475--519, 2011.
A Declarative Two-Level Framework to Specify and Verify
Workflow and Authorization Policies in Service-Oriented Architectures.
Service-Oriented Computing and Applications 5:105-137, 2011.
Back from the future.
Journal of Applied Non-Classical Logic 20(3):241-277, 2010.
Constraint Differentiation: Search-Space Reduction for the
Constraint-Based Analysis of Security Protocols.
Journal of Computer Security 18(4):575-618, 2010.
Labeled Tableaux for Distributed Temporal Logic.
Journal of Logic and Computation 19:1245-1279, 2009.
On the Semantics of Alice\&Bob Specifications of Security Protocols.
Theoretical Computer Science 367(1-2):88-122, 2006.
Relating Strand Spaces and Distributed Temporal Logic for
Security Protocol Analysis.
Logic Journal of the Interest Group in Pure and
Applied Logics (IGPL) 13(6):637-663, 2005.
OFMC: A Symbolic Model-Checker for Security Protocols.
International Journal of Information Security 4(3):181--208, 2005.
Modal sequent calculi labelled with truth
values: Completeness, duality and analyticity.
Logic
Journal of the Interest Group in Pure and Applied Logics (IGPL)
12(3): 227--274, 2004.
Truth-values as labels: a general
recipe for labelled deduction.
Journal of
Applied Non-Classical Logics, 13(3--4): 277--315, 2003.
Fibring Labelled Deduction Systems.
Journal of Logic and Computation 12(3):443-473,
2002.
An O(n log n)-Space Decision Procedure for
the Relevance Logic B+.
Studia
Logica 66(3):385-407, 2000.
Modal
Logics K, T, K4, S4: Labelled Proof Systems and New Complexity
Results.
The Bulletin of Symbolic Logic 5(1):91-93,
1999.
Labelled Modal Logics: Quantifiers.
Journal of Logic,
Language, and Information 7(3):237-263, 1998.
Natural
Deduction for Non-Classical Logics.
Studia Logica
60(1):119-160, 1998; special issue on Natural Deduction
edited by Frank Pfenning and Wilfried Sieg.
Labelled Propositional Modal Logics: Theory and Practice.
Journal of Logic and Computation 7(6):685-717, 1997.
Electronic Journal Papers
A History of Until.
In Proceedings of the 6th Workshop on Methods for Modalities (M4M'09).
Electronic Notes in Theoretical Computer Science 262:189-204, 2006.
Towards a Quantitative Analysis of Security
Protocols.
In Proceedings of the 4th Workshop on Quantitative Aspects of
Programming Languages (QAPL 2006).
Electronic Notes in Theoretical Computer Science 164(3):3-25, 2006.
Automated Security Protocol Analysis with the AVISPA
Tool.
In Proceedings of the XXI Mathematical Foundations of
Programming Semantics (MFPS'05).
Electronic Notes in Theoretical Computer Science 155:61-86, 2006.
Deconstructing Alice and Bob.
In Proceedings of the ICALP 2005 Workshop on Automated
Reasoning for Security Protocol Analysis (ARSPA'05).
Electronic Notes in Theoretical Computer Science 135(1):3-22,
2005.
Metareasoning about Security Protocols using Distributed
Temporal Logic.
In Proceedings of the IJCAR'04 Workshop on Automated Reasoning
for Security Protocol Analysis (ARSPA'04).
Electronic Notes in Theoretical Computer Science 125(1):67--89,
2005.
Towards an
awareness-based semantics for security protocol analysis.
In
Post-CAV Workshop on Logical Aspects of Cryptographic Protocol
Verification.
Electronic Notes in Theoretical Computer Science 55(1), 2001.
Bookchapters, Conferences and Workshops
Attack Interference: a Path to Defending Security Protocols.
In e-Business and Telecommunications -- ICETE 2011.
Springer, 2012, to appear.
Automated Analysis of Scenario-based Specifications of
Distributed Access Control Policies with Non-Mechanizable Activities.
In STM'12, Proceedings of the 8th International Workshop
on Security and Trust Management, held in conjunction with ESORICS 2012. LNCS, Springer, to appear.
Towards a Logical Framework for Reasoning about Risk
(Invited Paper).
In SeCIHD'12, Proceedings of the 2nd IFIP International
Workshop on Security and Cognitive Informatics for Homeland Defense, in
conjunction with ARES 2012. LNCS, Springer, to appear.
Automated Validation of Trust and Security of
Service-Oriented Architectures with the AVANTSSAR Platform (Invited
Paper).
In HPCS 2012, Proceedings of the 2012 International
Conference on High Performance Computing and Simulation. IEEE Computer Society Press, to appear.
An Environmental Paradigm for Defending Security
Protocols.
In SECOTS 2012, Proceedings of the Second
International Symposium on Security in Collaboration Technologies and
Systems (SECOTS is
part of CTS 2012, the 13th International Conference on Collaboration
Technologies and Systems), pages 427--438, IEEE Computer Society Press, 2012.
The AVANTSSAR Platform for the Automated Validation of Trust
and Security of Service-Oriented Architectures.
In TACAS 2012,
Proceedings of 18th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems. LNCS 7214, pages 267-282,
Springer 2012.
Security Protocols as Environments: a Lesson
from Non-collaboration.
In CollaborateCom 2011, Proceedings of the 7th
International Conference on Collaborative Computing: Networking,
Applications and Worksharing, pages 479-486. IEEE Computer Society Press, 2011.
A Hierarchy of Knowledge for the Formal Analysis of
Security-Sensitive Business Processes.
In CRiSIS 2011, Proceedings of the Sixth International Conference on Risks
and Security of Internet and Systems, pages 78-87, IEEE Computer Society Press, 2011.
Attack Interference in Non-Collaborative Scenarios for
Security Protocol Analysis.
In SECRYPT
2011, Proceedings of the International Conference on Security and
Cryptography (SECRYPT is part of
ICETE, The International Joint Conference on e-Business and
Telecommunications), pages 144-156. SciTePress, 2011.
Extended version (May 2011) available at
http://arxiv.org/abs/1106.3746.
Towards Formal Validation of Trust and Security in the
Internet of Services.
In Future Internet Assembly, LNCS 6656, pages 193-207. Springer-Verlag,
2011.
Blocking Underhand Attacks By Hidden Coalitions.
In Proceedings of ICAART'11, the 3rd International Conference on Agents and Artificial Intelligence, SciTePress Digital Library, pages 311-320, 2011.
A Deduction System for Meaning Negotiation.
In Proceedings of Declarative Agent Languages and Technologies VIII, LNCS
6619, pages 78-95. Springer-Verlag, 2011.
WSSMT: towards the
automated analysis of Security-Sensitive Services and Applications.
In Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 417-424. IEEE Computer Society, 2010.
Automated Validation of Security-sensitive Web Services
specified in BPEL and RBAC.
In Proceedings of 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 456-464,
IEEE Computer Society Press, 2010.
Model Checking Ad Hoc Network Routing Protocols: ARAN
vs. endairA.
In Proceedings of the 8th IEEE International Conference
on Software Engineering and Formal Methods, SEFM 2010, pages 191-202,
IEEE Computer Society Press, 2010.
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.
Secure
Pseudonymous Channels.
In Proceedings of Esorics'09, LNCS 5789, pages 337-354.
Springer-Verlag, 2009.
The Open-Source Fixed-Point Model Checker
for Symbolic Analysis of Security Protocols.
In FOSAD 2008/2009, LNCS 5705, pages
166--194. Springer-Verlag, 2009.
A labeled natural deduction system for a fragment of CTL*.
In Proceedings of LFCS
2009, Symposium on Logical Foundations of Computer Science, LNCS 5407,
pages 338--353. Springer-Verlag, 2009.
A Labeled Tableaux System for the Distributed Temporal Logic DTL.
In Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME 2008), pages 101-109, IEEE Computer Society Press, 2008.
\newblock Labeled Natural Deduction Systems for a Family of Tense Logics.
In Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME 2008), pages 118-126, IEEE Computer Society Press, 2008.
A Qualitative Modal Representation of Quantum Register Transformations.
In Proceedings of the 38th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2008), IEEE Computer Society Press, pages 131-137, 2008.
Formalizing and Analyzing Sender Invariance.
In Proceedings of the 4th international Workshop on Formal Aspects in Security and Trust (FAST2006), LNCS 4691,
pages 80-95, Springer-Verlag, 2007.
Symbolic and Cryptographic Analysis of the Secure
WS-ReliableMessaging Scenario.
In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (Fossacs 2006), LNCS 3921, pages 428-445, Springer-Verlag, 2006.
Algebraic Intruder Deductions.
In Proceedings of LPAR'05, LNAI 3835, pages
549-564. Springer-Verlag, 2005.
The AVISPA Tool for the Automated Validation of Internet
Security Protocols and Applications.
In Proceedings of CAV'05, LNCS 3576, pages
281-285. Springer-Verlag, 2005.
A Formalization of Off-Line Guessing for Security Protocol
Analysis.
In Proceedings of LPAR'04, LNAI 3452, pages
363-379. Springer-Verlag, 2005.
Towards a
Metalogic for Security Protocol Analysis.
In
Proceedings of Comblog'04, pages 187--196, Center for Logic and
Computation, Departamento de Matemàtica, Instituto Superior
Tècnico, Lisbon, Portugal, 2004, ISBN 972-99289-0-8.
Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols.
In Proceedings of CCS'03. ACM Press, 2003.
Constraint
Differentiation: A New Reduction Technique for Constraint-Based
Analysis of Security Protocols (Extended Abstract).
In Proceedings of SPV'03. 2003.
An
On-The-Fly Model-Checker for Security Protocol
Analysis.
In Proceedings of Esorics'03. LNCS
2808 Springer-Verlag, 2003.
Modal
Specifications of Trace-Based Security Properties.
In
Proceedings of the Second International Workshop on Security of
Mobile Multiagent Systems (SEMAS-2002). Research report
DFKI-RR-02-03, 2002.
The AVISS
Security Protocol Analysis Tool. In Proceedings of Computer-Aided
Verification CAV'02. LNCS 2404, Springer-Verlag, 2002.
Labelled deduction over algebras of
truth-values.
In Frontiers of Combining Systems 4
(Proceedings of FroCoS'2002). LNCS 2309, Springer-Verlag, 2002.
A Formal
Analysis of the CORBA Security Service.
In Proceedings of ZB
2002 (Formal Specification and Development in Z and B). LNCS 2272,
Springer-Verlag, 2002.
A Formal
Data-Model of the CORBA Security Service.
In Proceedings of
ESEC/FSE'01 (8th European Software Engineering Conference), ACM
Press, 2001.
A Recipe for the Complexity
Analysis of Non-Classical Logics.
In Frontiers of
Combining Systems 2 (Proceedings of FroCoS'98), Research Studies
Press/Wiley, 2000.
A
Modular Presentation of Modal Logics in a Logical Framework.
In The Tbilisi Symposium on Logic, Language and Computation:
Selected Papers, CSLI Publications, 1998.
A New
Method for Bounding the Complexity of Modal Logics.
In
Proceedings of KGC'97, LNCS 1289, Springer-Verlag, 1997.
Labelled Quantified Modal Logics.
In Proceedings of
KI'97, LNAI 1303, Springer-Verlag, 1997.
Implementing Modal and Relevance Logics in a Logical
Framework
In Proceedings of KR'96,
Morgan Kaufmann Publishers, 1996.
A
Topography of Labelled Modal Logics
In Frontiers of
Combining Systems (Proceedings of FroCoS'96), Kluwer Academic
Publishers, 1996.
Building and executing proof strategies in a formal metatheory.
In P. Torasso, editor, Proceedings of AI*IA 1993, 3rd Conference of
the Italian Association for Artificial Intelligence, LNCS 728, pages
11-22, Springer, Berlin, 1993.
SEL compiler and abstract analyzers.
In K. Broda, editor, Proceedings of ALPUK'92, 4th UK Conference on
Logic Programming, pages 108-123. Springer, Berlin, 1992.
Technical reports
Automated Analysis of Scenario-based Specifications of
Distributed Access Control Policies with Non-Mechanizable Activities
(Extended Version).
http://arxiv.org/abs/1206.3180, 2012.
Sufficient Conditions for Vertical Protocol Composition (Extended Version).
Technical Report IMM-TR-2011-18, DTU Informatics, http://imm.dtu.dk/~samo, 2012.
Attack Interference in Non-Collaborative Scenarios
for Security Protocol Analysis (Extended Version).
http://arxiv.org/abs/1106.3746, 2011.
Meaning Negotiation as Inference.
http://arxiv.org/abs/1101.4356, 2011.
Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version).
http://arxiv.org/abs/1009.4625v1, 2010.
Blocking Underhand Attacks by Hidden Coalitions (Extended Version).
http://arxiv.org/abs/1010.4786, 2010.
A History of Until (Extended Version).
http://arxiv.org/abs/0910.4500, 2009.
Secure Pseudonymous Channels (Extended Version).
Technical Report RZ3724, IBM Zurich Research Lab, 2009.
http://domino.research.ibm.com/library/cyberdig.nsf.
Labeled Natural Deduction Systems for a Family of Tense Logics (Extended Version).
http://arxiv.org/abs/0803.3187v1, 2008.
A Qualitative Modal Representation of Quantum Register Transformations (Extended Version).
http://arxiv.org/abs/0802.4057v1, 2008.
Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario (Extended Version).
Technical Report 502, ETH Zürich, Department of Computer Science, January 2006.
Deconstructing Alice and Bob (Extended Version).
Technical Report 486, ETH Zürich, Department of Computer Science, May 2005.
Algebraic Intruder Deductions (Extended Version).
Technical Report 485, ETH Zürich, Department of Computer Science, April 2005.
OFMC: A Symbolic Model-Checker for Security Protocols.
Technical Report 450, ETH Zürich, Department of Computer Science, June 2004.
Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols.
Technical Report 405, ETH Zürich, Department of Computer Science, May 2003.
An On-The-Fly Model-Checker for Security Protocol Analysis.
Technical Report 404, ETH Zürich, Department of Computer Science, April 2003.
Truth-values as labels: a general recipe for labelled deduction.
Technical Report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, Lisboa, Portugal, June 2003.
Modal Sequent Calculi Labelled with Truth-values: Completeness, Duality and Analyticity.
Technical Report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, Lisboa, Portugal, April 2003.
A Formal Analysis of the CORBA Security Service.
Technical Report No. 154, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, Germany, May 2001.
Fibring Labelled Deduction Systems.
Technical Report, Section of Computer Science, Department of Mathematics, Instituto Superior Técnico, Lisboa, Portugal, May 2000.
An O(n log n)-Space Decision Procedure for the Relevance Logic B+
(Extended Version).
Technical Report No. 140, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, Germany, May 2000.
Labelled Modal Logics: Quantifiers.
Research Report MPI-I-97-2-001, Max-Planck-Institut für Informatik, Saarbrücken, Germany, January 1997, ISSN 0946--011X.
Natural Deduction for Non-Classical Logics.
Research Report MPI-I-96-2-006, Max-Planck-Institut für Informatik, Saarbrücken, Germany, August 1996, ISSN 0946--011X.
Labelled Propositional Modal Logics: Theory and Practice.
Research Report MPI-I-96-2-002, Max-Planck-Institut für Informatik, Saarbrücken, Germany, January 1996, ISSN 0946--011X.
Building and executing proof strategies in a formal metatheory.
IRST-Technical Report 9305-11, IRST, Trento, Italy, and DIST Technical Report 93-0012, DIST, University of Genova, Italy, 2003.
Theses
Habilitationsschrift, Albert-Ludwigs-Universität Freiburg, 2003.
PhD Thesis, Universität des Saarlandes, 1997.
(Synthesis and execution of proof strategies in the formal metatheory of
an interactive theorem prover).
MSc Thesis, Università di Genova, 1994.
Edited Books and Proceedings
SecTest 2012, the Third International Workshop on Security Testing, affiliated with ICST 2012, Montreal, Quebec, April 21, 2012.
IEEE Computer Society Press, 2012.
SecTest 2011, the Second International Workshop on
Security Testing, affiliated with ICST 2011, Berlin, Germany, March 25,
2011.
IEEE Computer Society Press, 2011.
Foundations and Applications of Security Analysis, Joint Workshop
on Automated Reasoning for Security Protocol Analysis and Issues in the
Theory of Security, ARSPA-WITS 2009, Revised Selected Papers, LNCS 5511.
Springer-Verlag, Berlin, Germany, 2009.
Labelled Deduction.
Kluwer Academic Publishers, Dordrecht, The Netherlands, 2000.
Edited Journals
Special Issue of the Journal of Automated
Reasoning (JAR) 46(3-4) on Computer Security: Foundations and Automated Reasoning, Elsevier Science, 2011.
Special Issue of Information and Computation 206(2-4) on Computer Security: Foundations and Automated Reasoning, Elsevier Science, 2008.
Special Issue of the International Journal of Information Security
7(1) on Automated Reasoning for Security Protocol Analysis, Springer-Verlag, 2008.
Special Issue of Theoretical Computer Science 367(1-2) on Automated
Reasoning for Security Protocol Analysis, Elsevier Science, 2006.
Special Issue of the Journal of Automated Reasoning 36(1-2) on Automated Reasoning for Security Protocol Analysis, Elsevier Science, 2006.
Proceedings of the ICALP 2005 Workshop on Automated Reasoning for
Security Protocol Analysis (ARSPA'05)
Electronic Notes in Theoretical Computer Science 135(1),
Elsevier Science, 2005.
Proceedings of the IJCAR'04 Workshop on Automated Reasoning for
Security Protocol Analysis (ARSPA'04)
Electronic Notes in Theoretical Computer Science 125(1),
Elsevier Science, 2005.