Jan Cederquist

Contact

jan.cederquist"at"ist.utl.pt

Departamento de Engenharia Informática
Instituto Superior Técnico
Tagus Park
2780-990 Porto Salvo
Portugal

Tel: +351 214233262 (Ext. 5062)
Fax: +351 214233268

I am an assistant professor at IST, Technical University of Lisbon, since 2006, and a member of the SQIG - IT group.

Research interests

Mathematical modelling, formal specification and verification. My current research involves design and verification of security protocols, and language based security.

Teaching

Current teaching

Software Specification (ES5)

Former teaching

Analysis and Synthesis of Algorithms, Advanced Topics on Algorithms, Compilers, Introduction to Algorithms and Data Structures, Foundations of Programming, Language Based Security (PhD), Operating Systems, Software Quality, Software Security (MSc).

Students

Fernando Mário Machado Marques (MSc).

Carlos Magno Gaspar Vasconcelos (MSc).

Conferences

26th ACM Symposium on Applied Computing, Software Verification and Testing Track, TaiChung, Taiwan, March 21-25, 2011. Track chair.

25th ACM Symposium on Applied Computing, Software Verification and Testing Track, Sierre, Switzerland, March 22-26, 2010. Track chair.

SESYS 2006's (part of ICSNC 2006) Member of the Technical Program Committee.

Previous positions

Academia

(2004-2006) Post doc, dept of CS, University of Twente, The Netherlands. (2004) Post doc, SEN cluster, CWI, Amsterdam, The Netherlands. (2003) Post doc, EVEREST group, INRIA, Sophia-Antipolis, France. (1999-2000) Researcher, FDT lab, SICS, Stockholm, Sweden. (1997-1999) Post doc, dept of Computing, Imperial College, London, UK. (1991-1997) PhD student, dept of CS, Göteborg University, Sweden.

Industry

(2000-2003) Prover Technology, Stockholm, Sweden. (1988-1991) SEMCON, Trollhättan, Sweden. (1985-1988) KG Process AB, Trollhättan, Sweden.

Papers

E-voting

F. M. M. Marques, A. Almeida Matos and J. Cederquist. Integrating paper-based voting and Belenios -- a hybrid voting protocol for an academic organization. To appear in the proceedings of INFORUM 2017.

Design and Analysis of Security Protocols

M. Torabi Dashti Y. Wang and J. Cederquist. Risk balance in optimistic non-repudiation protocols. In 9th International Workshop on Formal Aspects of Security and Trust (FAST'11), pages 263--277, 2011.

J. Cederquist and M. Torabi Dashti. Complexity of Fairness Constraints for the Dolev-Yao In 26th ACM Symposium On Applied Computing (ACM SAC'11), pages 1502--1509, ACM, 2011.

J. Cederquist, M. Torabi Dashti and S. Mauw. A Certified Email Protocol using Key Chains. In 21st International conference on Advanced Information networking and Applications Workshops/Symposia (AINA'07), volume 1, pages 525--530. IEEE CS press, 2007.

J. Cederquist and M. Torabi Dashti. An Intruder Model for Verifying Liveness in Security Protocols. In A. D. Gordon and D. Sands, editors, 4th ACM workshop on Formal Methods in Security (FMSE'06), pages 23--31. ACM, 2006.

J. Cederquist, R. Corin and M. Torabi Dashti. On the quest for impartiality: Design and analysis of a fair non-repudiation protocol. In S. Qing, W. Mao, J. Lopez and G. Wang, editors, 7th International Conference on Information and Communications Security (ICICS'05), LNCS 3783, pages 27--39. Springer-Verlag, 2005.

J. Cederquist and M. T. Dashti. Formal Analysis of a Fair Payment Protocol. In T. Dimitrakos and F. Martinelli, editors, 2nd International Workshop on Formal Aspects of Security and Trust (FAST'04), IFIP, volume 173, pages 41--54. Kluwer Academic Publishers, 2004. [pdf]

Information Flow

A. Almeida Matos and J. Cederquist. Distributed Noninterference, In 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP'14), pp. 760-764, 2014.

A. Almeida Matos and J. Cederquist. Informative Types and Effects for Hybrid Migration Control, In 4th International Conference on Runtime Verification (RV'13), LNCS 8174, pp. 21-39, 2013.

A. Almeida Matos and J. Cederquist. Non-Disclosure for Distributed Mobile Code. In Mathematical Structures in Computer Science, special issue on Programming Language Interference and Dependence, Vol. 21, No. 6, pages 1111--1181, 2011.

Audit Logic

J. G. Cederquist, R. Corin, M. A. C. Dekker, S. Etalle, J. I. den Hartog and G. Lenzini. Audit-based compliance control. In T. Dimitrakos, F. Martinelli, P. Ryan and S. Schneider, editors, Internarional Journal of Information Security (IJIS'07), volume 6, issue 2. Springer Verlag, 2007.

J. G. Cederquist, R. Corin, M. A. C. Dekker, S. Etalle and J. I. den Hartog. An Audit Logic for Accountability. In A. Sakai and W. H. Winsborough, editors, 6th International Workshop on Policies for Distributed Systems and Networks (POLICY'05), pages 34--43. IEEE Computer Society Press, 2005.

Role Based Access Control

M. A. C. Decker, J. G. Cederquist, J. Crampon, S. Etalle. Extended Privilege Inheritance in RBAC (short paper). In R. H. Deng and P. Samarati, editors, Proceedings of the 2nd ACM Symposium on Information, Computer and Communications Security (ASIACCS'07). ACM press, 2007.

Formalization of Cryptology

G. Bathe, J. Cederquist and S. Tarento. A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin and M. Rusinowitch, editors, 2nd International Joint Conference on Automated Reasoning (IJCAR'04), LNCS 3097, pages 385-399, 2004.

Mobile Code Security

J. Cederquist and P. Giambiagi. Implementations that Preserve Confidentiality (Extended Abstract). Short presentation at Logic in Computer Science 2000 (LICS'00), 2000.

Type Theory and Formal Topology

J. Cederquist and T. Coquand. Entailment relations and distributive lattices. In S. R. Buss, P. Hájek and P. Pudlák, editors, Logic Colloquium '98, Lecture Notes in Logic, volume 13, pages 127--139. Association for Symbolic Logic, 1999.

J. Cederquist, T. Coquand and S. Negro. The Hahn-Banach Theorem in Type Theory. In G. Sabin and J. Smith, editors, Twenty-five years of Constructive Type Theory, Oxford University Press, 1998.

J. Cederquist. An implementation of the Heine-Bore covering theorem in type theory. In E. Gimenez and C. Pauline, editors, TYPES for Proofs and Programs, LICS, volume 1512, pages 46--65. Springer-Verlag, 1998.

J. Cederquist. A Point free Approach to Constructive Analysis in Type Theory. PhD thesis, Chalmers University of Technology and University of Göteborg, Sweden, 1997.

J. Cederquist and S. Negro. A constructive proof of the Heine-Bore covering theorem for formal reals. In S. Berardi and C. Coppo, editors, TYPES for Proofs and Programs, LICS, volume 1158, pages 62--75. Springer-Verlag, 1996.