Mads Dam:Selected Publications

Temporal logic; Security Logics; Authorisation; Pi-calculus; Confidentiality; Compositional verification; Linear logic; Networking; Other

New:

M. Cohen, M. Dam: "A Complete Axiomatization of Knowledge and Cryptography" Technical Report Trita-CSC-TCS-2007:1. Submitted for publication

Fetahi Wuhib, Mads Dam, Rolf Stadler, Alexander Clemm. "Robust Monitoring of Network-Wide Aggregates Using Gossiping" Technical report TRITA-EE_2006_043 To appear in Integrated Management (IM) 2007

M. Cohen and M. Dam: "Logical Omniscience in the Semantics of BAN Logics", in Proc. FCS'05, Chicago, 2005, pp. 121-132. [pdf,bib]

M. Cohen and M. Dam: "A Completeness Result for BAN Logic", in Proc. Methods for Modalities 4, Berlin, Dec. 2005 [pdf]

M. Dam: "Decidability and Proof Systems for Language-Based Noninterference Relations", in Proc. POPL'06, Charleston, South Carolina, Jan. 2006. [pdf]

Fetahi Wuhib, Mads Dam, Rolf Stadler, and Alexander Clemm. "Decentralized Computation of Threshold Crossing Alerts." In Proc. DSOM'05. [pdf]

Mu-calculus, Automata, Temporal Logics:

C. Sprenger and M. Dam: On the Structure of Inductive Reasoning: Circular and Tree-shaped Proofs in the mu-Calculus, In Proc. FOSSACS’03, Warsaw, Poland, LNCS vol. 2620, pp. 425-440. [ps, pdf, bib]

C. Sprenger and M. Dam: A note on global induction mechanisms in a µ-calculus with explicit approximations, Theoretical Informatics and Applications 37 (2003) pp. 365-399. [ps, pdf, bib]

M. Dam and D. Gurov: Mu-Calculus with Explicit Points and Approximations, Journal of Logic and Computation, vol. 12, issue 2, April 2002, pp. 255-269. [pdf, bib]

C. Sprenger and M. Dam: A note on global induction in a mu-calculus with explicit approximations. Proc. FICS 2002: pp. 22-24, 2002

M. Dam and D. Gurov: Mu-Calculus with Explicit Points and Approximations (Abstract). In Proc. FICS'00, 2000

M. Dam. CTL* and ECTL* as Fragments of the Modal mu-Calculus. Theoretical Computer Science 126 (1994) pp. 77-96. [ps, bib]

M. Dam. Temporal Logics, Automata, and Classical Theories - An Introduction. Lecture Notes for the 6th European Summer School on Logic, Language and Information, 1994. [pdf,ps]

M. Dam. Fixed Points of Buchi Automata. In Proceedings of 12th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 652 (1992) pp. 39-50. [ps, bib]

M. Dam. R-Generability, and Definability in Branching Time Logics. Information Processing Letters 41 (1992) pp. 281-287. [bib]

Security Logics:

M. Cohen, M. Dam: "A Complete Axiomatization of Knowledge and Cryptography" Technical Report Trita-CSC-TCS-2007:1. Submitted for publication

M. Cohen and M. Dam: "Logical Omniscience in the Semantics of BAN Logics", in Proc. FCS'05, Chicago, 2005, pp. 121-132. [pdf,bib]

M. Cohen and M. Dam: "A Completeness Result for BAN Logic", in Proc. Methods for Modalities 4, Berlin, Dec. 2005 [pdf]

Authorisation and delegation:

M. Dam: Regular SPKI. In Proc. 2003 Cambridge Security Protocols Workshop, Cambridge, U.K., LNCS vol 3364, pp. 134-150. [pdf]

O. Bandmann and M. Dam: A Note on SPKI's Authorisation Syntax. In Proc. 1st International PKI Research Workshop, NIST, Gaithersburg, MD, 2002. [pdf, bib]

O. Bandmann, M. Dam and B. Sadighi: Constrained Delegation. In Proc. IEEE Symposium on Security and Privacy, Berkeley, California, 2002, pp. 131-142. [ps, bib]

Pi-calculus, Higher-Order Processes:

M. Dam: “Proof Systems for Pi-Calculus Logics”. In R. de Queiroz (ed.), "Logic for Concurrency and Synchronisation", Trends in Logic, Logica Library, Kluwer, 2003, pp. 145--212. [ps, pdf, bib]

J.-L. Vivas and M. Dam: From Higher-Order pi-Calculus to pi-Calculus in the Presence of Static Operators. Proc. CONCUR'98, LNCS vol. 1466, pp. 115-130. [ps, bib]

M. Dam. On the Decidability of Process Equivalences for the pi-Calculus. Theoretical Computer Science 183, 1997, pp. 215-228. [pdf, ps, bib].

M. Dam. "Model Checking Mobile Processes". Information and Computation 129(1), 1996, pp. 35-51. [pdf,ps, bib]. Revised version of CONCUR'93 paper. [pdf,ps,bib]

R. Amadio and M. Dam. ``Toward a Modal Theory of Types for the pi-Calculus''. [ps]. SICS Research Report RR 96:03. Also in Proc. FTRTFT'96, Springer Lecture Notes in Computer Science. [ps,bib]

R. Amadio, M. Dam. ``Reasoning about Higher-Order Processes''. Proc. CAAP'95, pp. 202-217. [pdf,ps, bib]. Also as SICS research report RR 94:18.

Confidentiality, Information flow:

M. Dam: "Decidability and Proof Systems for Language-Based Noninterference Relations", to appear in Proc. POPL'06, Charleston, South Carolina, Jan. 2006.

P. Giambiagi, M. Dam: “On the Secure Implementation of Security Protocols”, Science of Computer Programming 50 (1-3), 2004, pp. 73-99. [pdf,bib].

P. Giambiagi, M. Dam: “On the Secure Implementation of Security Protocols”, in Proc. ESOP’03, Warsaw, Poland, Springer LNCS vol. 2618, pp. 144-158. [pdf, bib]

M. Dam and P. Giambiagi: Confidentiality for Mobile Code: The Case of a Simple Payment Protocol. Proc. 13th Computer Science Foundations Workshop, IEEE, pp. 233-244, 2000. [pdf,ps,bib]

M. Dam. Proving Trust in Systems of Second-Order Processes: Preliminary Results. Manuscript, 53 pp, 1997. [pdf,ps] Conference version appearing as Proving Trust in Systems of Second-Order Processes (Extended Abstract) in Proc. HICSS'98, vol. VII, IEEE 1998, pp. 255-264. [pdf,ps,bib].

Compositional Verification, Erlang, Dynamic Process Networks, CCS:

T. Arts, G. Chugunov, M. Dam, L.-å. Fredlund, D. Gurov, T. Noll: A Verification Tool for Erlang”. Int. Journal of Software Tools for Technology Transfer, vol. 4, number 4, August 2003, pp. 405-420. [pdf,ps,bib]

T. Arts and M. Dam: "Verifying a Distributed Database Lookup Manager Written in Erlang". Proc. FM'99 vol. I, LNCS vol. 1708, pp. 682-700, 1999 [pdf,ps,bib]

M. Dam and D. Gurov: "Compositional Verification of CCS Processes". Proc. PSI'99, LNCS vol. 1755, pp. 247-256, 1999 [pdf,ps,bib]

M. Dam: ``Proving Properties of Dynamic Process Networks''. Information and Computation 140, 1998, pp. 95-114. [pdf,ps,bib]. Full version of ``Compositional proof systems for model checking...'', Proc. CONCUR'95, pp. 12-26. [bib]

M. Dam, L.-å. Fredlund and D. Gurov. "Toward Parametric Verification of Open Distributed Systems." In Compositionality: The Significant Difference (H. Langmaack, A. Pnueli, W.-P. De Roever (eds.)), LNCS vol. 1536, pp. 150-185, 1998. [pdf,ps,bib]

T. Arts, M. Dam, L.-å. Fredlund and D. Gurov. "System Description: Verification of Distributed Erlang Programs." In Proc. of CADE'98, Springer LNAI, vol. 1421, pp. 38-41, 1998. [pdf,ps,bib]

M. Dam, L.-å. Fredlund and D. Gurov. "Compositional Verification of Erlang Programs." In Proc. Third International Workshop on Formal Methods for Industrial Critical Systems (FMICS), CWI, 1998. [bib]

M. Dam and L.-å. Fredlund. "On the Verification of Open Distributed Systems." Proc. SAC'98, IEEE, pp. 532-540, 1998. [pdf,ps,bib]

Linear and Relevant Logics for Processes:

M. Dam. ``Process-Algebraic Interpretations of Positive Linear and Relevant Logics''. Journal of Logic and Computation 4 (1994) pp. 939-973. [pdf,ps,bib]

M. Dam. ``Relevance Logic and Concurrent Composition''. PhD thesis, Dept. of Computer Science, University of Edinburgh, 1990, CST-66-90. Also published as ECS-LFCS-90-119. [pdf,ps,bib]

M. Dam. ``Relevance Logic and Concurrent Composition''. Proc. LICS'88, pp. 178-185. [pdf,ps,bib]

Networking:

Fetahi Wuhib, Mads Dam, Rolf Stadler, and Alexander Clemm. "Decentralized Computation of Threshold Crossing Alerts." In Proc. DSOM'05. [pdf]

M. Dam, G. Karlsson, B. S. Firozabadi, R. Stadler. "A Research Agenda for Distributed Policy-Based Management". Proc. Radiovetenskap och Kommunikation (RVK), 2002. [pdf,bib]

M. Dam, R. Stadler. "A Generic Protocol for Network State Aggregation". Proc. Radiovetenskap och Kommunikation (RVK), 2005. [pdf,bib]

Other:

Mads Dam, Lars-åke Fredlund, Dilian Gurov: Formal Methods Research at SICS and KTH: An Overview. Electr. Notes Theor. Comput. Sci. 80: (2003)

M. Dam. ``Modalities in Analysis and Verification''. ACM Computing Surveys Symposium on Models of Programming Languages and Computation, 1996.  [pdf,ps,bib]

M. Dam, F. Jensen. ``Compiler Generation from Relational Semantics''. Proceedings of the European Symposium on Programming, Lecture Notes in Computer Science 213 (1986) pp. 1-29.  [bib]

 


 

Mads Dam
Last revised, August 2005