Research

2012

• David Basin and Cas Cremers and Catherine Meadows. Model Checking Security Protocols. Springer, 2012.
  To appear.
  (abstract) (BibTeX entry)
  
• David Basin and Matúvs Harvan and Felix Klaedtke and Eugen Zalinescu. MONPOLY: Monitoring Usage-control Policies. In Proceedings of the 2nd International Conference on Runtime Verification (RV 2011).Lecture Notes in Computer Science, 7186. Springer, 2012.
  (BibTeX entry) (Springer)
  
• David Basin and Felix Klaedtke and Eugen Zalinescu. Algorithms for Monitoring Real-time Properties. In Proceedings of the 2nd International Conference on Runtime Verification (RV 2011).Lecture Notes in Computer Science, 7186. Springer, 2012.
  (BibTeX entry)
  
• Tom Hvitved and Felix Klaedtke and Eugen Zalinescu. A trace-based model for multiparty contracts. In The Journal of Logic and Algebraic Programming, 81 (2), pages 72-98, 2012.
  (BibTeX entry) (Elsevier)
  
• Petar Tsankov and Mohammad Torabi Dashti and David Basin. SecFuzz: Fuzz-testing Security Protocols. In Proceedings of the 7th International Workshop on Automation of Software Test.AST'12ACM, 2012.
  (BibTeX entry) (PDF)
  
• Anton Wijs and Mohammad Torabi Dashti. Extended beam search for non-exhaustive state space analysis. In The Journal of Logic and Algebraic Programming, 81 (1), pages 46-69, 2012.
  (BibTeX entry)
  

2011

• Mahdi Asadpour and Mohammad Torabi Dashti. A Privacy-friendly RFID protocol using reusable anonymous tickets. In IEEE TrustCom '11.IEEE, 2011.
  (BibTeX entry)
  
• David Basin and Samuel J. Burri and Guenter Karjoth. Obstruction-free Authorization Enforcement: Aligning Security and Business Objectives. In 24th Computer Security Foundations Symposium (CSF 2011).IEEE, 2011.
  (abstract) (BibTeX entry) (URL) (PDF) (IEEE)
  
• David Basin and Samuel J. Burri and Guenter Karjoth. Separation of Duties as a Service. In ACM Symposium on Information, Computer and Communications Security (ASIACCS '11').ACM, 2011.
  (abstract) (BibTeX entry) (PDF)
  
• David Basin and Carlos Caleiro and Jaime Ramos and Luca Viganò. Distributed temporal logic for the analysis of security protocol models. In Theoretical Computer Science, 412 (31), pages 4007-4043, 2011.
  (abstract) (BibTeX entry) (URL) (PDF) (Copyright © 2011, Elsevier)
  
• David Basin and Srdjan Capkun and Patrick Schaller and Benedikt Schmidt. Formal Reasoning about Physical Properties of Security Protocols. In ACM Transactions on Information and System Security, 14 (2), pages 16:1-16:29, 2011.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• David A. Basin and Manuel Clavel and Marina Egea. A decade of model-driven security. In Proceedings of the 16th ACM symposium on Access control models and technologies (SACMAT 2011)., 1998443. New York, NY, USA, 2011.
  (BibTeX entry) (PDF) (http://doi.acm.org/10.1145/1998441.1998443)
  
• David Basin and Manuel Clavel and Marina Egea and Miguel Garcia de Dios and Carolina Dania and Gonzalo Ortiz and Javier Valdazo. Model-Driven Development of Security-Aware GUIs for Data-Centric Applications. Springer Berlin / Heidelberg, 2011.
  (abstract) (BibTeX entry) (URL) (PDF) (© Springer)
  
• David Basin and Cas Cremers. Evaluation of ISO/IEC 9798 Protocols. CRYPTREC, 2011.
  Version 2.0
  (BibTeX entry) (PDF)
  
• David Basin and Matúvs Harvan and Felix Klaedtke and Eugen Zalinescu. Monitoring Usage-control Policies in Distributed Systems. In 18th International Symposium on Temporal Representation and Reasoning (TIME 2011).IEEE Computer Society, 2011.
  (abstract) (BibTeX entry)
  

• David Basin and Patrick Schaller and Michael Schläpfer Applied Information Security: A Hands-on Approach. Springer, 2011. (abstract) (BibTeX entry) (URL)

  
  
• Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. An Approach to Modular and Testable Security Models of Real-world Health-Care Applications. In ACM symposium on access control models and technologies (SACMAT).ACM Press, 2011.
  (abstract) (BibTeX entry) (PDF)
  
• Joachim M. Buhmann and Morteza Haghir Chehreghani and Mario Frank and Andreas P. Streich. Information Theoretic Model Selection for Pattern Analysis. In ICML 2011 Workshop on Unsupervised and Transfer Learning., 2011.
  (abstract) (BibTeX entry) (PDF)
  
• Samuel J. Burri and Guenter Karjoth. Flexible Scoping of Authorization Constraints on Workflows with Loops and Parallelism. In 1st BPM Workshop on Workflow Security Audit and Certification (WfSAC '11).LNCSSpringer, 2011.
  (abstract) (BibTeX entry) (PDF)
  
• Jan Cederquist and Mohammad Torabi Dashti. Complexity of fairness constraints for the Dolev-Yao attacker model. In ACM Symposium On Applied Computing (SAC).SAC '11ACM, 2011.
  (BibTeX entry) (URL) (PDF) (ACM New York, USA)
  
• Jan Cederquist and Mohammad Torabi Dashti and Yanjing Wang. Risk balance in optimistic non-repudiation protocols. In Formal Aspects of Security & Trust (FAST).Springer, 2011.
  (BibTeX entry)
  
• Bruno Conchinha and David Basin and Carlos Caleiro. FAST: An Efficient Decision Procedure for Deduction and Static Equivalence. In 22nd International Conference on Rewriting Techniques and Applications, RTA 2011.LIPIcs, 10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Bruno Conchinha and David Basin and Carlos Caleiro. Efficient Decision Procedures for Message Deducibility and Static Equivalence. In 7th International Workshop on Formal Aspects of Security and Trust - FAST 2010.Lecture Notes in Computer Science, 6561. Springer, 2011.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Cas J.F. Cremers. Key Exchange in IPsec revisited: Formal Analysis of IKEv1 and IKEv2. In ESORICS 2011.LNCS, 6879. Springer Verlag, 2011.
  To appear.
  (BibTeX entry) (PDF) (© Springer)
  
• Cas J.F. Cremers. Examining Indistinguishability-Based Security Models for Key Exchange Protocols: The case of CK, CK-HMQV, and eCK. In ASIACCS 2011.ACM, 2011.
  (BibTeX entry) (URL) (PDF)
  
• Cas Cremers and Michele Feltz. One-round Strongly Secure Key Exchange with Perfect Forward Secrecy and Deniability. Cryptology ePrint Archive, 2011.
  Report 2011/300
  (BibTeX entry) (URL)
  
• Cas Cremers and Kasper Bonne Rasmussen and Srdjan Capkun. Distance Hijacking Attacks on Distance Bounding Protocols. Cryptology ePrint Archive, 2011.
  Report 2011/129
  (BibTeX entry) (URL)
  
• Boris Danev and Ramya Jayaram Masti and Ghassan Karame and Srdjan Capkun. Enabling Secure VM-vTPM Migration in Private Clouds. In Proceedings of the Annual Computer Security Applications Conference (ACSAC)., 2011.
  (BibTeX entry)
  
• Boris Danev and Davide Zanetti and Srdjan Capkun. On Physical-layer Identification of Wireless Devices. In ACM Computing Surveys, 2011.
  (BibTeX entry)
  
• Mohammad Torabi Dashti. Faulhaber's Triangle. In The College Mathematics Journal, 42 (2), 2011.
  (BibTeX entry)
  
• Christian Dax and Felix Klaedtke. Alternation Elimination for Automata over Nested Words. In 14th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'11).Lecture Notes in Computer Science, 6604. Springer, 2011.
  (BibTeX entry) (Springer)
  
• Aurelien Francillon and Boris Danev and Srdjan Capkun. Relay Attacks on Passive Keyless Entry and Start Systems in Modern Cars. In Proceedings of Network and Distributed System Security Symposium (NDSS)., 2011.
  (BibTeX entry)
  
• Mario Frank and Joachim M. Buhmann. Selecting the rank of truncated SVD by Maximum Approximation Capacity. In ISIT 2011: IEEE International Symposium on Information Theory.IEEE, 2011.
  (abstract) (BibTeX entry) (URL) (IEEE)
  
• Mario Frank and Morteza and Haghir Chehreghani and Joachim M. Buhmann. The Minimum Transfer Cost Principle for Model-Order Selection. In ECML PKDD 2011: European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases.Springer, 2011.
  (abstract) (BibTeX entry) (PDF) (Springer)
  
• Simone Frau and Mohammad Torabi Dashti. Integrated specification and verification of security protocols and policies. In IEEE 24th Computer Security Foundations Symposium (CSF 2011).IEEE Computer Society, 2011.
  (BibTeX entry) (URL) (IEEE)
  
• Thai Son Hoang and Jean-Raymond Abrial. Reasoning about Liveness Properties in Event-B. In Formal Methods and Software Engineering (ICFEM).LNCS, 6991. Springer, 2011.
  (BibTeX entry) (Springer)
  
• Simon Hudon and Thai Son Hoang. Development of Control Systems Guided by Models of their Environment. In Electronic Notes in Theoretical Computer Science, 280, pages 57-68, 2011.
  (BibTeX entry) (URL) (Elsevier)
  
• Ghassan Karame and Srdjan Capkun and Ueli Maurer. Privacy-Preserving Outsourcing of Brute-Force Key Searches. In Proceedings of the ACM Cloud Computing Security Workshop (CCSW); in conjunction with ACM CCS.ACM, 2011.
  (BibTeX entry)
  
• Ghassan Karame and Aurelien Francillon and Srdjan Capkun. Pay as you Browse: Microcomputations as Micropayments in Web-based Services. In Proceedings of the International World Wide Web Conference.ACM, 2011.
  (BibTeX entry)
  
• Claudio Marforio and Aurelien Francillon and Srdjan Capkun. Application Collusion Attack on the Permission-Based Security Model and its Implications for Modern Smartphone Systems. ETH Zurich, 2011.
  (BibTeX entry) (PDF)
  
• Christina Pöpper and Nils O. Tippenhauer and Boris Danev and Srdjan Capkun. Investigation of Signal and Message Manipulations on the Wireless Channel. In Proceedings of the European Symposium on Research in Computer Security (ESORICS).Springer-Verlag, 2011.
  (BibTeX entry)
  
• Michael Schläpfer and Rolf Haenni and Reto Koenig and Oliver Spycher. Efficient Vote Authorization in Coercion-Resistant Internet Voting. In 3rd International Conference on E-Voting and Identity (VoteID 2011).Springer-Verlag, 2011.
  (abstract) (BibTeX entry)
  
• Michael Schläpfer and Oliver Spycher and Reto Koenig and Rolf Haenni. A New Approach Towards Coercion-Resistant Remote E-Voting in Linear Time. In 15th International Conference on Financial Cryptography and Data Security.Springer-Verlag, 2011.
  (abstract) (BibTeX entry)
  
• Renato Silva and Carine Pascal and Thai Son Hoang and Michael Butler. Decomposition tool for Event-B. In Softw. Pract. Exper., 41 (2), 2011.
  (BibTeX entry) (Wiley)
  
• Christoph Sprenger and David Basin. Refining Key Establishment. Computer Science Department, ETH Zurich, Technical Report 736, 2011.
  (BibTeX entry) (URL)
  
• Nils Ole Tippenhauer and Christina Pöpper and Kasper Bonne Rasmussen and Srdjan Capkun. On the Requirements for Successful GPS Spoofing Attacks. In In Proceedings of the ACM Conference on Computer and Communications Security (CCS)., 2011.
  (BibTeX entry) (PDF)
  
• Petar Tsankov and David Basin and Mohammad Torabi Dashti. Constructing mid-points for two-party asynchronous protocols. In Principles of Distributed Systems - 15th International Conference, OPODIS 2011.Lecture Notes in Computer Science, 7109. Springer, 2011.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Eugen Zalinescu. Shorter strings containing all k-element permutations. In Information Processing Letters, 111 (12), 2011.
  (BibTeX entry) (URL)
  
• Davide Zanetti and Pascal Sachs and Srdjan Capkun. On the Practicality of UHF RFID Fingerprinting: How Real is the RFID Tracking Problem?. In Privacy Enhancing Technologies (PETS).Lecture Notes in Computer Science, 6794. Springer, 2011.
  (BibTeX entry) (PDF)
  
• matthias schmalz. Term Rewriting in Logics of Partial Functions. In ICFEM, 2011.
  (BibTeX entry) (Springer)
  

2010

• Jean-Raymond Abrial and Michael Butler and Stefan Hallerstede and Thai Son Hoang and Farhad Mehta and Laurent Voisin. RODIN: An Open Toolset for Modelling and Reasoning in Event-B. In STTT, 12 (6), 2010.
  (BibTeX entry) (Springer)
  
• B. Badban and M. Torabi Dashti. Semi-linear Parikh images of regular expressions via reduction. In MFCS.LNCS, 6281. Springer, 2010.
  (BibTeX entry)
  
• David Basin and Manuel Clavel and Marina Egea and Michael Schläpfer. Automatic Generation of Smart, Security-Aware GUI Models. In International Symposium on Engineering Secure Software and Systems (ESSoS 2010).Springer-Verlag, 2010.
  (abstract) (BibTeX entry) (Springer)
  
• David Basin and Cas Cremers. Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries. In 19th EACSL Annual Conference on Computer Science Logic (CSL).LNCS, 6247. Springer-Verlag, 2010.
  (abstract) (BibTeX entry) (URL) (PDF) (Springer-Verlag)
  
• David Basin and Cas Cremers. Modeling and Analyzing Security in the Presence of Compromising Adversaries. In Computer Security - ESORICS 2010.Lecture Notes in Computer Science, 6345. Springer, 2010.
  (abstract) (BibTeX entry)
  
• David Basin and Felix Klaedtke and Samuel Müller. Monitoring Security Policies with Metric First-order Temporal Logic. In 15th ACM Symposium on Access Control Models and Technologies (SACMAT).ACM Press, 2010.
  (BibTeX entry) (ACM)
  
• David Basin and Felix Klaedtke and and Samuel Müller. Policy Monitoring in First-Order Temporal Logic. In 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010.LNCS, 6174/2010. Springer Berlin / Heidelberg, 2010.
  (abstract) (BibTeX entry) (URL) (Springer)
  
• Achim D. Brucker and Lukas Brügger and Paul Kearney and Burkhart Wolff. Verified Firewall Policy Transformations for Test Case Generation. In International Conference on Software Testing, Verification, and Validation (ICST10)., 2010.
  (abstract) (BibTeX entry) (PDF)
  
• Achim D. Brucker and Lukas Brügger and Matthias P. Krieger and Burkhart Wolff. HOL-TestGen 1.5.0 User Guide. ETH Zurich, Technical Report 670, 2010.
  (BibTeX entry) (URL) (PDF)
  
• Bruno Conchinha and David Basin and Carlos Caleiro. Efficient Decision Procedures for Message Deducibility and Static Equivalence. ETH Zürich, 2010.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Bruno Conchinha and David Basin and Carlos Caleiro. Efficient Decision Procedures for Message Deducibility and Static Equivalence. In Formal Aspects in Security and Trust (FAST '2010).LNCS, 6561. Springer Berlin / Heidelberg, 2010.
  (abstract) (BibTeX entry) (URL) (PDF) (Springer)
  
• Cas J.F. Cremers. Session-StateReveal is stronger than eCK's EphemeralKeyReveal: Using automatic analysis to attack the NAXOS protocol. In International Journal of Applied Cryptography (IJACT), 2 (2), pages 83-99, 2010.
  (BibTeX entry)
  
• Mohammad Torabi Dashti. Accountability in optimistic non-repudiation protocols. ETH, Technical Report 701, 2010.
  (BibTeX entry) (URL)
  
• Mohammad Torabi Dashti and Sjouke Mauw. Fair Exchange. Chapman & Hall/CRC Cryptography and Network Security Series, 2010.
  (BibTeX entry) (URL) (PDF) (http://dx.doi.org/10.1201/9781420059823-c5)
  
• Christian Dax and Felix Klaedtke and Martin Lange. On Regular Temporal Logics with Past. In Acta Informatica, 47 (4), pages 251-277, 2010.
  (BibTeX entry) (Springer)
  
• Miguel A. García de Dios and Carolina Dania and Michael Schläpfer and David Basin and Manuel Clavel and Marina Egea. SSG: a model-based development environment for smart, security-aware GUIs. In ACM/IEEE 32nd International Conference on Software Engineering., 2. ACM, 2010.
  (abstract) (BibTeX entry) (ACM)
  
• W. Fokkink and M. Torabi Dashti and A. Wijs. Partial order reduction for branching security protocols. In ACSD.IEEE CS, 2010.
  (BibTeX entry)
  
• Mario Frank and Joachim M. Buhmann and David Basin. On the Definition of Role Mining. In SACMAT '10: Proceeding of the 15th ACM symposium on Access control models and technologies.ACM, 2010.
  (abstract) (BibTeX entry) (URL) (ACM)
  
• Simone Frau and Mohammad Torabi Dashti. Integrated Specification and Verification of Security Protocols and Policies. ETH, Technical Report 702, 2010.
  (BibTeX entry) (URL)
  
• Thai Son Hoang. How to interpret Failed Proofs in Event-B. Department of Computer Science, ETH Zurich, Technical Report 672, 2010.
  (abstract) (BibTeX entry) (URL)
  
• Thai Son Hoang and Jean-Raymond Abrial. Event-B Decomposition for Parallel Programs. In Abstract State Machines, Alloy, B and Z (ABZ2010).LNCS, 5977. Springer, 2010.
  (abstract) (BibTeX entry) (Springer)
  
• Felix Klaedtke. Ehrenfeucht-Fraisse Goes Automatic for Real Addition. In Information and Computation, 208 (11), pages 1283-1295, 2010.
  (BibTeX entry)
  
• Shin’ichiro Matsuo and Kunihiko Miyazaki and Akira Otsuka and David Basin. How to Evaluate the Security of Real-life Cryptographic Protocols? The cases of ISO/IEC 29128 and CRYPTREC. In FC 2010 Workshops, RLCPS, WECSR, and WLC 2010.LNCS, 6054. Springer, 2010.
  Booktitle: Financial Cryptography and Data Security
  (abstract) (BibTeX entry)
  
• Simon Meier and Cas Cremers and David Basin. Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs. In CSF 2010.IEEE Computer Society, 2010.
  (BibTeX entry) (PDF)
  
• Sebastian Mödersheim and Luca Viganò and David A. Basin. Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols. In Journal of Computer Security, 18 (4), pages 575-618, 2010.
  (abstract) (BibTeX entry) (URL)
  
• Christina Pöpper and Srdjan Capkun and David Basin and Cas J.F. Cremers. Keeping Data Secret under Full Compromise using Porter Devices. In ACSAC 2010.ACM, 2010.
  (abstract) (BibTeX entry)
  
• Benedikt Schmidt and Patrick Schaller and David Basin. Impossibility Results for Secret Establishment. In 23nd IEEE Computer Security Foundations Symposium (CSF 2010).IEEE Computer Society, 2010.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Renato Silva and Carine Pascal and Thai Son Hoang and Michael Butler. Decomposition Tool: Development and Usage. University of Dusseldorf, Germany, 2010.
  In Proceedings of the Rodin User and Developer Workshop
  (BibTeX entry)
  
• Renato Alexandre Silva and Carine Pascal and Thai Son Hoang and Michael Butler. Decomposition Tool for Event-B. 2010, In Proceedings of the Workshop on Tool Building in Formal Methods - ABZ Conference, Orford, Canada
  (BibTeX entry)
  
• Christoph Sprenger and David Basin. Developing Security Protocols by Refinement. In 7th ACM Conference on Computer and Communications Security (CCS 2010).ACM, 2010.
  (abstract) (BibTeX entry) (PDF)
  
• Michael Wahler and David Basin and Achim D. Brucker and Jana Koehler. Efficient Analysis of Pattern-Based Constraint Specifications. In Software and Systems Modeling, 9 (2), pages 225-255, 2010.
  keywords = UML, OCL, Constraints, Patterns, Consistency
  (BibTeX entry) (PDF) (Springer-Verlag, Heidelberg)
  
• Emre Yilmaz and Thai Son Hoang. Development of Rabin's Choice Coordination Algorithm in Event-B. In Electronic Communications of the EASST, 35, 2010.
  (BibTeX entry) (URL) (EASST)
  
• Dengguo Feng and David Basin and Peng Liu. Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security. In ACM, Inc., 2010.
  Number of Pages: 363; ISBN:978-1-60558-936-7
  (BibTeX entry) (URL) (Copyright © 2010 ACM, Inc.)
  

2009

• David Basin and Samuel Burri and Guenter Karjoth. Dynamic Enforcement of Abstract Separation of Duty Constraints. In 14th European Symposium on Research in Computer Security (ESORICS).5789, 5789. Springer-Verlag, 2009.
  (abstract) (BibTeX entry) (URL) (PDF) (© Springer)
  
• David Basin and Carlos Caliero and Jaime Ramos and Luca Vigano. Labelled Tableaux for Distributed Temporal Logic. In Journal of Logic and Computation, 19 (6), pages 1245-1279, 2009.
  (BibTeX entry) (IEEE Computer Society)
  
• David Basin and Srdjan Capkun and Patrick Schaller and Benedikt Schmidt. Let's Get Physical: Models and Methods for Real-World Security Protocols. In Theorem Proving in Higher Order Logics (TPHOLs 2009).LNCS, 5674. Springer, 2009.
  invited talk
  (abstract) (BibTeX entry) (URL) (© Springer)
  
• David Basin and Manuel Clavel and Jürgen Doser and Marina Egea. Automated analysis of security-design models. In Information and Software Technology, 51 (5), pages 815-831, 2009.
  (BibTeX entry) (PDF)
  
• Patrik Bichsel and Samuel Müller and Franz-Stefan Preiss and Dieter Sommer and Mario Verdicchio. Security and Trust through Electronic Social Network-based Interactions. In Workshop on Security and Privacy in Online Social Networking (SPOSN '09).IEEE Computer Society Press, 2009.
  (BibTeX entry)
  
• Achim D. Brucker and Burkhart Wolff. Semantics, Calculi, and Analysis for Object-Oriented Specifications. In Acta Informatica, 46 (4), pages 255-284, 2009.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Cas J.F. Cremers. Formally and Practically Relating the CK, CK-HMQV, and eCK Security Models for Authenticated Key Exchange. 2009
  (BibTeX entry) (URL)
  
• Cas J.F. Cremers. Session-state Reveal is stronger than Ephemeral Key Reveal: Attacking the NAXOS key exchange protocol. In ACNS'09.LNCS, 5536. Springer, 2009.
  (BibTeX entry)
  
• Cas Cremers and David Basin. From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries. 2009
  (abstract) (BibTeX entry) (URL)
  
• Cas J.F. Cremers and Pascal Lafourcade and Philippe Nadeau. Comparing State Spaces in Automatic Security Protocol Analysis. Springer, 2009.
  (BibTeX entry)
  
• M. Torabi Dashti. Optimistic fair exchange using trusted devices. ETH Zurich, Technical Report 635, 2009.
  (BibTeX entry) (URL) (ETH)
  
• Mohammad Torabi Dashti. Optimistic Fair Exchange Using Trusted Devices. In Stabilization, Safety, and Security of Distributed Systems.LNCS, 5873. Springer, 2009.
  (BibTeX entry)
  
• Christian Dax and Felix Klaedtke and Martin Lange. On Regular Temporal Logics with Past. In 36th International Colloquium on Automata, Languages, and Programming (ICALP'09).Lecture Notes in Computer Science, 5556. Springer-Verlag, 2009.
  (BibTeX entry) (Springer-Verlag)
  
• Christian Dax and Felix Klaedtke and Stefan Leue. Specification Languages for Stutter-Invariant Regular Properties. In 7th International Symposium on Automated Technology for Verification and Analysis (ATVA).Lecture Notes in Computer Science, 5799. Springer-Verlag, 2009.
  (BibTeX entry)
  
• Mario Frank and Matthias Plaue and Holger Rapp and Ullrich Köthe and Bernd Jähne and Fred A. Hamprecht. Theoretical and Experimental Error Analysis of Continuous-Wave Time-Of-Flight Range Cameras. In Optical Engineering, 48 (1), 2009.
  (abstract) (BibTeX entry) (URL) (Optical Engineering)
  
• Mario Frank and Matthias Plaue and Fred A. Hamprecht. Denoising of Continuous-Wave Time-Of-Flight Depth Images using Confidence Measures. In Optical Engineering, 48 (7), 2009.
  (abstract) (BibTeX entry) (URL) (Society of Photo-Optical Instrumentation Engineers (SPIE))
  
• Mario Frank and Andreas P. Streich and David Basin and Joachim M. Buhmann. A Probabilistic Approach to Hybrid Role Mining. In 16th ACM Conference on Computer and Communications Security (CCS 2009).ACM, 2009.
  (abstract) (BibTeX entry) (URL) (ACM)
  
• Stefan Hallerstede and Thai Son Hoang. Qualitative Reasoning for the Dining Philosophers. 2009, Dagstuhl Seminar 09381
  (BibTeX entry) (URL)
  
• Matus Harvan and Alexander Pretschner. State-based Usage Control Enforcement with Data Flow Tracking using System Call Interposition. In 3rd International Conference on Network & System Security.IEEE, 2009.
  (abstract) (BibTeX entry)
  
• Thai Son Hoang. Event-B Decomposition for Parallel Programs. 2009, Dagstuhl Seminar 09318
  (BibTeX entry) (URL)
  
• Thai Son Hoang and Jean-Raymond Abrial. Event-B Development of the FindP Program. Department of Computer Science, ETH Zurich, Technical Report 653, 2009.
  (abstract) (BibTeX entry)
  
• Thai Son Hoang and David Basin and Jean-Raymond Abrial. Specifying Access Control in Event-B. Department of Computer Science, ETH Zurich, Technical Report 624, 2009.
  (abstract) (BibTeX entry)
  
• Thai Son Hoang and Andreas Fürst and Jean-Raymond Abrial. Event-B Patterns and Their Tool Support. In SEFM 2009.IEEE Computer Society Press, 2009.
  (BibTeX entry)
  
• Thai Son Hoang and Hironobu Kuruma and David A. Basin and Jean-Raymond Abrial. Developing Topology Discovery in Event-B. In 7th International Conference on Integrated Formal Methods (IFM).LNCS, 5423. Springer, 2009.
  (BibTeX entry) (PDF)
  
• Thai Son Hoang and Hironobu Kuruma and David Basin and Jean-Raymond Abrial. Developing Topology Discovery in Event-B. In Science of Computer Programming, 74 (11-12), pages 879-899, 2009.
  (abstract) (BibTeX entry) (URL)
  
• S. Mauw and S. Radomirovic and M. Torabi Dashti. Minimal message complexity of asynchronous multi-party contract signing. In CSF.IEEE CS, 2009.
  (BibTeX entry) (IEEE)
  
• Bruno Montalto and Carlos Caleiro. Modeling and Reasoning About an Attacker with Cryptanalytical Capabilities. 2009
  (abstract) (BibTeX entry) (PDF)
  
• Samuel Müller. Theory and Applications of Runtime Monitoring Metric First-order Temporal Logic. ETH Zurich,2009.
  DISS. ETH No. 18445
  (BibTeX entry)
  
• Alexander Pretschner and Matthias Büchler and Matus Harvan and Christian Schaefer and Thomas Walter. Usage Control Enforcement with Data Flow Tracking for X11. In 5th International Workshop on Security and Trust Management (STM 2009)., 2009.
  (abstract) (BibTeX entry)
  
• Patrick Schaller and Benedikt Schmidt and David Basin and Srdjan Capkun. Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks. In 22nd IEEE Computer Security Foundations Symposium., 2009.
  (abstract) (BibTeX entry) (PDF)
  
• Michael Schläpfer and Marina Egea and David Basin and Manuel Clavel. Automatic Generation of Security-Aware GUI Models. In European Workshop on Security in Model Driven Architecture 2009 (SECMDA 2009)., 2009.
  (abstract) (BibTeX entry)
  
• Matthias Schmalz and Daniele Varacca and Hagen Völzer. Counterexamples in Probabilistic LTL Model Checking for Markov Chains. In Concur 2009.LNCS, 5710. Springer, 2009.
  (BibTeX entry) (Springer)
  
• Andreas P. Streich and Mario Frank and David Basin and Joachim M. Buhmann. Multi-Assignment Clustering for Boolean Data. In Proceedings of the 26th International Conference on Machine Learning.ACM, 2009.
  (abstract) (BibTeX entry) (URL) (http://doi.acm.org/10.1145/1553374.1553498)
  
• David A. Basin and Srdjan Capkun and Wenke Lee. Proceedings of the Second ACM Conference on Wireless Network Security, WISEC 2009, Zurich, Switzerland March 16-19, 2009. In ACM, 2009.
  Book Title: WiSec'09
  (BibTeX entry)
  

2008

• S. Andova and C.Cremers and K. Gjosteen and S. Mauw and S. Mjolsnes and S. Radomirovic. A framework for compositional verification of security protocols. In Information and Computation, 206 (2-4), pages 425-459, 2008.
  (abstract) (BibTeX entry)
  
• David Basin and Carlos Caleiro and Jaime Ramos and Luca Viganò. A Labeled Tableaux System for the Distributed Temporal Logic DTL. In time, 0, pages 101-109, 2008.
  Publisher IEEE Computer SocietyAddress Los Alamitos, CA, USA
  (abstract) (BibTeX entry) (URL) (PDF) (Copyright © 2008, IEEE, Inc.)
  
• David Basin and Manuel Clavel and Jürgen Doser and Marina Egea. Automated Analysis of Security-Design Models. In Information and Software Technology, 2008.
  to appear.
  (abstract) (BibTeX entry) (Elsevier)
  
• David Basin and Felix Klaedtke and Samuel Müller and Birgit Pfitzmann. Runtime Monitoring of Metric First-order Temporal Properties. IBM Research & ETH Zurich, Technical Report RZ 3702, 2008.
  (abstract) (BibTeX entry) (PDF)
  
• David Basin and Felix Klaedtke and Samuel Müller and Birgit Pfitzmann. Runtime Monitoring of Metric First-order Temporal Properties. In Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008).Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2008.
  (abstract) (BibTeX entry) (URL)
  
• B. Baudry and A. Faivre and S. Ghosh and A. Pretschner. 4th International Workshop on Model Driven Engineering, Verification, and Validation: Integrating Verification and Validation in MDE. In MODELS 2007 workshops.LNCS, 5002. Springer, 2008.
  (BibTeX entry)
  
• Sascha Böhme and Rustan Leino and Burkhart Wolff. HOL-Boogie — An Interactive Prover for the Boogie Program Verifier. In 21th International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2008). LNCS 5170 Springer-Verlag, 2008.
  (abstract) (BibTeX entry) (PDF) (© Springer-Verlag)
  
• Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Model-based Firewall Conformance Testing. In Testcom/FATES 2008. LNCS 5047 Springer-Verlag, 2008.
  (abstract) (BibTeX entry) (URL) (PDF) (© Springer-Verlag)
  
• Achim D. Brucker and Lukas Brügger and Burkhart Wolff. Verifying Test-Hypotheses: An Experiment in Test and Proof. In Fourth Workshop on Model Based Testing (MBT 2008).Electronic Notes in Theoretical Computer Science, 220 (1). , 2008.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Achim D. Brucker and Burkhart Wolff. A Formal Proof Environment for UML/OCL. In Proceedings of Formal Aspects of Software Engineering (FASE 2008).Lecture Notes in Computer Science, 4961. Springer Berlin / Heidelberg, 2008.
  (abstract) (BibTeX entry) (PDF)
  
• Achim D. Brucker and Burkhart Wolff. Extensible Universes for Object-Oriented Data Models. In Proceedings of the European Conference of Object-Oriented Programming (ECOOP 2008). LNCS 5142 Springer-Verlag, 2008.
  (abstract) (BibTeX entry) (URL) (PDF) (© Springer-Verlag)
  
• Achim D. Brucker and Burkhart Wolff. An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. In Journal of Automated Reasoning (JAR), Selected Papers of the AVOCS-VERIFY Workshop 2006 (3-4), pages 219-249, 2008.
  Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds)
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Ilinca Ciupa and Bertrand Meyer and Manuel Oriol and Alexander Pretschner. Manual Testing vs. Random Testing+ vs. User Reports. In 19th Intl. Symp. on SW Reliability Engineering (ISSRE).IEEE, 2008.
  (BibTeX entry)
  
• I. Ciupa and A. Pretschner and A. Leitner M. Oriol and B. Meyer. On the Predictability of Random Tests for Object-Oriented Software. In 1st International Conference on Software Testing, Verification, and Validation.IEEE, 2008.
  Best Paper Award
  (BibTeX entry)
  
• Cas Cremers. On the Protocol Composition Logic PCL. In ASIACCS'08.ACM, 2008.
  (BibTeX entry)
  
• C.J.F. Cremers. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In 20th International Conference on Computer Aided Verification (CAV 2008).Lecture Notes in Computer ScienceSpringer-Verlag, 2008.
  (BibTeX entry)
  
• Cas J.F. Cremers. Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement. In 15th ACM Conference on Computer and Communications Security (CCS 2008).ACM, 2008.
  (abstract) (BibTeX entry)
  
• Cas J.F. Cremers. Session-state reveal is stronger than Ephemeral-key reveal: Breaking the NAXOS protocol. 2008
  (abstract) (BibTeX entry) (URL)
  
• Mohammad Torabi Dashti and Srijith Krishnan Nair and Hugo Jonker. Nuovo DRM Paradiso: Designing a Secure, Verified, Fair Exchange DRM Scheme. In Fundam. Inform., 89 (4), pages 393-417, 2008.
  (BibTeX entry) (URL)
  
• Matthias Daum and Jan Dörrenbächer and Mareike Schmidt and Burkhart Wolff. A Verification Approach for System-Level Concurrent Programs. In Verified Software: Theories, Tools, Experiments. LNCS 5295 Springer Berlin / Heidelberg, 2008.
  (abstract) (BibTeX entry) (URL) (PDF) (© Springer-Verlag)
  
• Christian Dax and Felix Klaedtke. Alternation Elimination by Complementation. In Proc. of the 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08)., 2008.
  (BibTeX entry)
  
• Jochen Eisinger and Felix Klaedtke. Don't Care Words with an Application to the Automata-Based Approach for Real Addition. In Formal Methods in System Design, 33 (1-3), pages 85-115, 2008.
  (BibTeX entry) (Springer-Verlag)
  
• Daniel Fischer and David Basin and Thomas Engel. Topology dynamics and routing for predictable mobile networks. In Network Protocols, 2008. ICNP 2008. IEEE International Conference on.IEEE, 2008.
  (abstract) (BibTeX entry) (PDF) (IEEE)
  
• Mario Frank and David Basin and Joachim M. Buhmann. A Class of Probabilistic Models for Role Engineering. In 15th ACM Conference on Computer and Communications Security (CCS 2008).ACM, 2008.
  (abstract) (BibTeX entry) (URL) (http://doi.acm.org/10.1145/1455770.1455809)
  
• Dilian Gurov and Marieke Huisman and Christoph Sprenger. An algorithmic approach to compositional verification of programs with procedures. In Foundations of Interface Technologies (FIT 2008)., 2008.
  (BibTeX entry) (PDF)
  
• Dilian Gurov and Marieke Huisman and Christoph Sprenger. Compositional Verification of Programs with Procedures. In Journal of Information and Computation, 206 (7), pages 840-868, 2008.
  (BibTeX entry) (URL)
  
• Ralf Hielscher and Daniel Potts and Jürgen Prestin and Helmut Schaeben and Matthias Schmalz. The Radon Transform on SO(3): a Fourier Slice Theorem and Numerical Inversion. In Inverse Problems, 24 (025011), 2008.
  (BibTeX entry) (URL) (PDF) (Inverse Problems)
  
• Thai Son Hoang and Hironobu Kuruma and David Basin and Jean-Raymond Abrial. Developing Topology Discovery in Event-B. Department of Computer Science, ETH-Zurich, Technical Report 611, 2008.
  (abstract) (BibTeX entry) (URL)
  
• Felix Klaedtke. Ehrenfeucht-Fraisse Goes Automatic for Real Addition. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS'08).IBFI Schloss Dagstuhl, 2008.
  (BibTeX entry) (URL)
  
• Felix Klaedtke. Bounds on the Automata Size for Presburger Arithmetic. In ACM Transactions on Computational Logic, 9 (2), 2008.
  (BibTeX entry) (URL) (ACM)
  
• Y. Le Traon and T. Mouelhi and A. Pretschner and B. Baudry. Test-Driven Assessment of Access Control in Legacy Applications. In 1st International Conference on Software Testing, Verification, and Validation.IEEE, 2008.
  (BibTeX entry)
  
• V. Lotz and E. Pigout and P. Fischer and D. Kossmann and F. Massacci and A. Pretschner. Towards Systematic Achievement of Compliance in Service-oriented Architectures: The MASTER approach. In Wirtschaftsinformatik, 2008.
  (BibTeX entry)
  
• Michael N"af and David Basin. Two approaches to an information security laboratory. In Communications of the ACM, 51 (12), pages 138-142, 2008.
  (BibTeX entry) (ACM New York, NY, USA)
  
• Simona Orzan and Muhammad Torabi Dashti. Fair Exchange Is Incomparable to Consensus. In Theoretical Aspects of Computing - ICTAC 2008, 5th International Colloquium.LNCS, 5160. Springer, 2008.
  (BibTeX entry) (URL) (Springer)
  
• Simona Orzan and Mohammad Torabi Dashti. Data Failures. In Distributed Computing (DISC '08).LNCS, 5218. Springer, 2008.
  (BibTeX entry) (Springer)
  
• Panos Papadimitratos and Marcin Poturalski and Patrick Schaller and Pascal Lafourcade and David Basin and Srdjan Capkun and Jean-Pierre Hubaux. Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking. In IEEE Communications Magazine, 40 (2), pages 132-139, 2008.
  (abstract) (BibTeX entry) (URL)
  
• Alexander Pretschner. Doctoral Symposium. In MODELS 2008.Springer, 2008.
  (BibTeX entry)
  
• A. Pretschner and R. Breu. Doktorandensymposium bei der Modellierung 2008. In Modellierung 2008.GI, 2008.
  (BibTeX entry)
  
• A. Pretschner and M. Hilty and D. Basin and C. Schaefer and T. Walter. Mechanisms for Usage Control. In ASIACCS., 2008.
  (BibTeX entry)
  
• Alexander Pretschner and T. Mouelhi and Y. Le Traon. Model-Based Tests for Access Control Policies. In 1st International Conference on Software Testing, Verification, and Validation.IEEE, 2008.
  (BibTeX entry)
  
• A. Pretschner and F. Schütz and C. Schaefer and T. Walter. Policy Evolution in Distributed Usage Control. In 4th Intl. Workshop on Security and Trust Management. 2008.
  (BibTeX entry)
  
• A. Pretschner and T. Walter. Negotiation of Usage Control Policies - Simply the Best. In 1st Intl. Workshop on Advances in Policy Enforcement., 2008.
  Keynote
  (BibTeX entry)
  
• Oppliger Rolf and Hauser Ralf and Basin David. SSL/TLS Session-Aware User Authentication. In IEEE Computer, 41 (3), pages 78-84, 2008.
  (BibTeX entry) (URL) (PDF) (Copyright ©2007, IEEE, Inc.)
  
• Christoph Sprenger and David Basin. Cryptographically-sound Protocol-Model Abstractions. In Computer Security Foundations (CSF 08)., 0. IEEE Computer Society, 2008.
  (abstract) (BibTeX entry) (URL) (Copyright © 2008, IEEE, Inc.)
  
• Christoph Sprenger and David Basin. Cryptographically-sound Protocol-Model Abstractions. In Logic in Computer Science (LICS 08)., 0. IEEE Computer Society, 2008.
  (abstract) (BibTeX entry) (URL) (Copyright © 2008, IEEE, Inc.)
  
• Michael Wahler. A Pattern Approach to Increasing the Maturity Level of Class Models. Idea Group, 2008.
  (BibTeX entry) (URL)
  
• Michael Wahler. Using Patterns to Develop Consistent Design Constraints. ETH Zurich,2008.
  (abstract) (BibTeX entry) (PDF)
  
• Dr. Rolf Oppliger et al.. SSL/TLS Session-Aware User Authentication Revisited. In Computers & Security, 27 (3-5), pages 64-70, 2008.
  (abstract) (BibTeX entry) (URL) (PDF) (Copyright © 2008 Elsevier B.V.)
  

2007

• Carl Abrams and Jürg von Känel and Samuel Müller and Birgit Pfitzmann and Susanne Ruschka-Taylor. Optimized Enterprise Risk Management. In IBM Systems Journal, 46 (2), pages 219-234, 2007.
  (abstract) (BibTeX entry)
  
• B. Agreiter and M. Alam and R. Breu and M. Hafner and A. Pretschner and J.-P. Seifert and X. Zhang. A Technical Architecture for Enforcing Usage Control Requirements in Service-Oriented Architectures. In ACM Workshop on Secure Web Services. ACM, 2007.
  (BibTeX entry)
  
• David Basin and Manuel Clavel and Jürgen Doser and Marina Egea. A Metamodel-Based Approach for Analyzing Security-Design Models. In MODELS 2007.LNCS, 4735. Springer-Verlag, 2007.
  (abstract) (BibTeX entry) (PDF) (Springer-Verlag)
  
• David Basin and Hironobu Kuruma and Shin Nakajima and Burkhart Wolff. The Z Specification Language and the Proof Environment Isabelle/HOL-Z. In Computer Software - Journal of the Japanese Society for Software Science and Technology, 24 (2), pages 21-26, 2007.
  In Japanese.
  (abstract) (BibTeX entry) (http://www.jstage.jst.go.jp/browse/jssst/24/2/_contents)
  
• David Basin and Hironobu Kuruma and Kunihiko Miyazaki and Kazuo Takaragi and Burkhart Wolff. Verifying a signature architecture: a comparative case study. In Formal Aspects of Computing, 19 (1), pages 63-91, 2007.
  http://www.springerlink.com/content/u368650p18557674/?p=8851693f5ba14a3fb9d493dae37783b8&pi=0
  (abstract) (BibTeX entry) (PDF) (© Springer-Verlag)
  
• David Basin and Ernst-Rüdiger Olderog and Paul E. Sevinç. Specifying and Analyzing Security Automata using CSP-OZ. In AsiaCCS 2007.ACM, 2007.
  (abstract) (BibTeX entry) (URL) (PDF) (ACM, 2007)
  
• Bernd Becker and Christian Dax and Jochen Eisinger and Felix Klaedtke. LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. In Proc. of the 19th International Conference on Computer Aided Verification (CAV'07).Lecture Notes in Computer Science, 4590. Springer-Verlag, 2007.
  (BibTeX entry)
  
• Bernd Becker and Jochen Eisinger and Felix Klaedtke. Parallelization of Decision Procedures for Automatic Structures. In 1st Workshop on Omega Automata (OMEGA'07)., 2007.
  (BibTeX entry)
  
• Diana von Bidder and David Basin and Germano Caronni. Midpoints versus Endpoints: From Protocols to Firewalls. In ACNS 2007.LNCS, 4521. Springer-Verlag, 2007.
  (abstract) (BibTeX entry) (PDF) (Springer)
  
• M. Broy and I. Krüger and A. Pretschner and C. Salzmann. Engineering Automotive Software. In Proceedings of the IEEE, 95 (2), pages 356-373, 2007.
  (BibTeX entry)
  
• Achim D. Brucker. An Interactive Proof Environment for Object-oriented Specifications. ETH Zurich,2007.
  ETH Dissertation No. 17097.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Jürgen Doser. Metamodel-based UML Notations for Domain-specific Languages. In 4th International Workshop on Software Language Engineering (ATEM 2007). 2007.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Jürgen Doser and Burkhart Wolff. An MDA Framework Supporting OCL. In Electronic Communications of the EASST, 5, 2007.
  (abstract) (BibTeX entry) (PDF)
  
• Achim D. Brucker and Jürgen Doser and Burkhart Wolff. Semantic Issues of OCL: Past, Present, and Future. In Electronic Communications of the EASST, 5, 2007.
  (abstract) (BibTeX entry) (PDF)
  
• Achim D. Brucker and Burkhart Wolff. Test-Sequence Generation with HOL-TestGen - With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. lncs 4454, Springer-Verlag, 2007.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript) (doi:10.1007/978-3-540-73770-4_9) (© Springer-Verlag)
  
• Cas Cremers. Scyther: Unbounded Verification of Security Protocols. ETH Zurich, Technical Report 572, 2007.
  (abstract) (BibTeX entry)
  
• Cas Cremers. Complete Characterization of Security Protocols by Pattern Refinement (Work in Progress). 2007, Dagstuhl Seminar: Formal Protocol Verification Applied
  (abstract) (BibTeX entry)
  
• Cas Cremers and Pascal Lafourcade. Comparing State Spaces in Automatic Security Protocol Verification. ETH Zurich, Technical Report 558, 2007.
  Technical report no. 558.
  (abstract) (BibTeX entry) (URL)
  
• Cas Cremers and Pascal Lafourcade. Comparing State Spaces in Security Protocol Analysis. In Seventh International Workshop on Automated Verification of Critical Systems.ENTCSElsevier ScienceDirect, 2007.
  (abstract) (BibTeX entry)
  
• Christian Dax and Jochen Eisinger and Felix Klaedtke. Mechanizing the Powerset Construction for Restricted Classes of omega-Automata. In Proc. of the 5th International Symposion on Automated Technology for Verification and Analysis (ATVA'07).Lecture Notes in Computer Science, 4762. Springer-Verlag, 2007.
  (BibTeX entry)
  
• Paul Hankes Drielsma and Sebastian Mödersheim and Luca Viganò and David Basin. Formalizing and Analyzing Sender Invariance. In Formal Aspects of Security and Trust.LNCS, 4691. Springer Verlag, 2007.
  To appear. An intermediate version of this paper is available as ETH technical report no. 528.
  (abstract) (BibTeX entry) (PDF) (© Springer)
  
• Stefan Hallerstede and Thai Son Hoang. Qualitative Probabilistic Modelling in Event-B. In Integrated Formal Methods, 6th International Conference, IFM 2007.Lecture Notes in Computer Science, 4591. Springer, 2007.
  This research was carried out as part of the EU research project IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems) http://rodin.cs.ncl.ac.uk.
  (abstract) (BibTeX entry) (URL) (PDF) (2007)
  
• Manuel Hilty and Alexander Pretschner and David Basin and Christian Schaefer and Thomas Walter. Monitors for Usage Control. In Joint iTrust and PST Conferences on Privacy, Trust Management and Security.IFIP International Federation for Information Processing, 238. Springer-Verlag, 2007.
  (abstract) (BibTeX entry)
  
• Manuel Hilty and Alexander Pretschner and David Basin and Christian Schaefer and Thomas Walter. A Policy Language for Distributed Usage Control. In 12th European Symposium on Research in Computer Security (ESORICS 2007).LNCS, 4734. Springer-Verlag, 2007.
  (abstract) (BibTeX entry) (URL) (Springer-Verlag 2007)
  
• Felix Klaedtke and Stefan Ratschan and Zhikun She. Language-Based Abstraction Refinement for Hybrid System Verification. In 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007).Lecture Notes in Computer ScienceSpringer-Verlag, 2007.
  (BibTeX entry)
  
• Boris Köpf and David Basin. An Information-Theoretic Model for Adaptive Side-Channel Attacks. In CCS '07: Proceedings of the 14th ACM Conference on Computer and Communications Security.ACM Press, 2007.
  (abstract) (BibTeX entry) (PDF)
  
• Alice Y. Liu and Samuel Müller and Ke Xu. A Static Compliance-Checking Framework for Business Process Models. In IBM Systems Journal, 46 (2), pages 335-361, 2007.
  (abstract) (BibTeX entry)
  
• Simon Meier. A Formalization of an Operational Semantics of Security Protocols. ETH Zurich, 2007.
  (abstract) (BibTeX entry) (URL) (PDF) (2007, Simon Meier)
  
• Sebastian Mödersheim. Models and Methods for the Automated Analysis of Security Protocols. PhD Thesis, ETH Zürich,2007.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Samuel Müller and Chonawee Supatgiat. A Quantitative Optimization Model for Dynamic Risk-based Compliance Management. In IBM Journal of Research and Development, 51 (3/4), pages 295-308, 2007.
  (abstract) (BibTeX entry)
  
• David Basin ETH Zürich AND Ernst-Rüdiger Olderog University of Oldenburg AND Paul E. Sevinc ETH Zürich. Specifying and analysing Security Automata using CSP-OZ. In Information, computer and Communication security, ASIACCS'07.The Association for Computing Machinery, 2007.
  (abstract) (BibTeX entry) (URL) (Copyright 2007 by the Association for Computing Machinery)
  
• Alexander Pretschner and M. Broy and I.Krüger and T. Stauner. Software Engineering for Automotive Systems - A Roadmap. In 29th Int. Conference on Software Engineering: Future of Software Engineering. IEEE, 2007.
  (BibTeX entry)
  
• Alexander Pretschner and Manuel Hilty and David Basin. Verteilte Nutzungskontrolle. In Digma: Zeitschrift fuer Datenrecht und Informationssicherheit, 7 (4), pages 146-149, 2007.
  (abstract) (BibTeX entry) (PDF)
  
• A. Pretschner and M. Hilty and F. Massacci. Usage Control in Service-Oriented Architecture. In 3rd Intl. Conf. on Trust, Privacy & Security in Digital Business.LNCS, 4657. Springer, 2007.
  (BibTeX entry)
  
• Oppliger Rolf and Hauser Ralf and Basin David and Rodenhaeuser Aldo and Kaiser Bruno. A Proof of Concept Implementation of SSL/TLS Session-Aware User Authentication (TLS-SA). In Kommunikation in Verteilten Systemen (KiVS) 2007.Informatik aktuellSpringer Verlag, 2007.
  (abstract) (BibTeX entry) (URL) (© Springer)
  
• Patrick Schaller and Srdjan Capkun and David Basin. BAP: Broadcast Authentication Using Cryptographic Puzzles. In International Conference on Applied Cryptography and Network Security (ACNS 2007), 4521, pages 401-419, 2007.
  (abstract) (BibTeX entry) (PDF) (©Springer-Verlag)
  
• Matthias Schmalz and Hagen Völzer and Daniele Varacca. Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths. In FSTTCS'07.LNCS, 4855. Springer, 2007.
  The pdf link refers to the technical report version.
  (BibTeX entry) (PDF) (Springer)
  
• Paul E. Sevinç and Mario Strasser and David Basin. Securing the Distribution and Storage of Secrets with Trusted Platform Modules. In WISTP 2007.LNCS, 4462. Springer, 2007.
  (abstract) (BibTeX entry) (URL) (PDF) (IFIP International Federation for Information Processing 2007)
  
• Christoph Sprenger and David Basin. A monad-based modeling and verification toolbox with application to security protocols. In Theorem Proving in Higher-Order Logics (TPHOLs).Lecture Notes in Computer Science, 4732. Springer-Verlag, 2007.
  To appear.
  (abstract) (BibTeX entry) (PDF)
  
• Michael Wahler and Jana Koehler and Achim D. Brucker. Model-Driven Constraint Engineering. In Electronic Communications of the EASST, 5, 2007.
  (BibTeX entry) (URL) (PDF)
  
• Makarius Wenzel and Burkhart Wolff. Building Formal Method Tools in the Isabelle/Isar Framework. In TPHOLs 2007. LNCS 4732 Springer-Verlag, 2007.
  (abstract) (BibTeX entry) (PDF) (© Springer-Verlag)
  
• Pierpaolo Degano and Ralf Küsters and Luca Viganò and Steve Zdancewic. Special Issue of Information and Computation on Automated Reasoning for Security Protocol Analysis. In Elsevier Science, 2007.
  To appear
  (BibTeX entry)
  

2006

• Carl Abrams and Jürg von Känel and Samuel Müller and Birgit Pfitzmann and Susanne Ruschka-Taylor. Optimized Enterprise Risk Management. IBM Research, Technical Report RZ 3657, 2006.
  (abstract) (BibTeX entry)
  
• Pedro Ad~ao and Paulo Mateus and Tiago Reis and Luca Viganò. Towards a Quantitative Analysis of Security Protocols. In Electronic Notes in Theoretical Computer Science (Proceedings of the 4th Workshop on Quantitative Aspects of Programming Languages, QAPL 2006), 164 (3), pages 3-25, 2006.
  (BibTeX entry) (URL) (http://www.sciencedirect.com/science?_ob=PublicationURL&_tockey=#TOC#13109#2006#998359996#635745#FLP#&_cdi=13109&_pubType=J&view=c&_auth=y&_acct=C000011279&_version=1&_urlVersion=0&_userid=217827&md5=f801df110ee543417be23d455a07e9f4)
  
• Michael Backes and Sebastian M"odersheim and Birgit Pfitzmann and Luca Vigan`o. Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario (extended version). Department of Computer Science, ETH Zurich, Technical Report 502, 2006.
  (abstract) (BibTeX entry) (PDF)
  
• Michael Backes and Sebastian Mödersheim and Birgit Pfitzmann and Luca Viganò. Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario. In Proceedings of FOSSACS 2006.LNCS, 3921. Springer-Verlag, 2006.
  (BibTeX entry)
  
• David Basin and Jürgen Doser and Torsten Lodderstedt. Model Driven Security: from UML Models to Access Control Infrastructures. In ACM Transactions on Software Engineering and Methodology, 15 (1), pages 39-91, 2006.
  An intermediate version is available as ETH technical report no. 414
  (abstract) (BibTeX entry) (© ACM, (2006))
  
• Manfred Broy and Alexander Pretschner and Christian Salzmann and Thomas Stauner. Software intensive systems in the automotive domain: challenges for research and education. In SAE world congress. SAE, 2006.
  (BibTeX entry)
  
• Achim D. Brucker and Jürgen Doser and Burkhart Wolff. An MDA Framework Supporting OCL. In 6th OCL Workshop at the UML/MoDELS Conference., 2006.
  (abstract) (BibTeX entry) (PDF)
  
• Achim D. Brucker and Jürgen Doser and Burkhart Wolff. Semantic Issues of OCL: Past, Present, and Future. In 6th OCL Workshop at the UML/MoDELS Conference., 2006.
  (abstract) (BibTeX entry) (PDF)
  
• Achim D. Brucker and Jürgen Doser and Burkhart Wolff. A Model Transformation Semantics and Analysis Methodology for SecureUML. In MoDELS 2006: Model Driven Engineering Languages and Systems. LNCS 4199 Springer-Verlag, 2006.
  An extended version of this paper is available as ETH Technical Report, no. 524.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  
• Achim D. Brucker and Burkhart Wolff. A Package for Extensible Object-Oriented Data Models with an Application to IMP++. In International Workshop on Software Verification and Validation (SVV 2006). Computing Research Repository (CoRR) 2006.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Burkhart Wolff. The HOL-OCL Book. ETH Zürich, Technical Report 525, 2006.
  (abstract) (BibTeX entry) (PDF)
  
• Carlos Caleiro and Luca Viganò and David Basin. On the Semantics of Alice&Bob Specifications of Security Protocols. In Theoretical Computer Science, 367 (1-2), pages 88-122, 2006.
  (BibTeX entry)
  
• S.-K. Chen and H. Lei and M. Wahler and H. Chang and K. Bhaskaran and J. Frank. A model driven XML transformation framework for Business Performance Management model creation. In International Journal of Electronic Business, 4 (3/4), pages 281-301, 2006.
  (abstract) (BibTeX entry) (URL)
  
• C. Dax and M. Hofmann and M. Lange. A Proof System for the Linear Time mu-Calculus. In FSTTCS 2006., 4337. Springer, 2006.
  (BibTeX entry) (Springer)
  
• Paul Hankes Drielsma and Sebastian Mödersheim and Luca Viganò and David Basin. Formalizing and Analyzing Sender Invariance. ETH Zurich, Technical Report 528, 2006.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Jochen Eisinger and Felix Klaedtke. Don't Care Words with an Application to the Automata-based Approach for Real Addition. In 18th International Conference on Computer Aided Verification (CAV)., 2006.
  (BibTeX entry) (PDF) (Springer-Verlag)
  
• S. Gauch and M. Speretta and A. Pretschner. Ontology-Based User Profiles for Personalized Search. Springer, 2006.
  (BibTeX entry)
  
• Christopher Giblin and Samuel Müller and Birgit Pfitzmann. From Regulatory Policies to Event Monitoring Rules: Towards Model-Driven Compliance Automation. IBM Research, Technical Report RZ 3662, 2006.
  (abstract) (BibTeX entry)
  
• M. Hilty and A. Pretschner and C. Schaefer and T. Walter. Enforcement for Usage Control-An overview of Control Mechanisms. DoCoMo Euro-Labs, Technical Report I-ST-018, 2006.
  (BibTeX entry)
  
• M. Hilty and A. Pretschner and C. Schaefer and T. Walter. Usage Control Requirements in Mobile and Ubiquitous Computing Applications. In International Conference on Systems and Networks Communications.IEEE, 2006.
  Best paper award.
  (BibTeX entry)
  
• Jana Koehler and Rainer Hauser and Jochen Küster and Ksenia Ryndina and Jussi Vanhatalo and Michael Wahler. The Role of Visual Modeling and Model Transformations in Business-driven Development. In Fifth International Workshop on Graph Transformation and Visual Modeling Techniques., 2006.
  (BibTeX entry) (URL) (PDF)
  
• Boris Köpf and David Basin. Timing-Sensitive Information Flow Analysis for Synchronous Systems. ETH Zurich, Technical Report 526, 2006.
  (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Boris Köpf and David Basin. Timing-Sensitive Information Flow Analysis for Synchronous Systems. In ESORICS '06.LNCS, 4189. Springer Verlag, 2006.
  (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• J. M. Küster and J. Koehler and R. Hauser and K. Ryndina and J. Vanhatalo and M. Wahler. Methodology and Tooling to Combine an Existing Legacy Business Process Model with Best-Practice Industry Reference Models for Business Transformation. IBM Research technical report RZ 3663, 2006.
  (BibTeX entry) (PDF)
  
• Alice Y. Liu and Samuel Müller and Ke Xu. A Static Compliance Checking Framework for Business Process Models. IBM Research, Technical Report RZ 3679, 2006.
  (abstract) (BibTeX entry)
  
• Sebastian Mödersheim. On the Relationships between Models in Protocol Verification (Extended Version). Infsec, ETH Zuerich, Technical Report 512, 2006.
  (abstract) (BibTeX entry) (PDF)
  
• Samuel Müller. A Dependability Perspective On Enterprise Compliance. IBM Research, Technical Report RZ 3667, 2006.
  (abstract) (BibTeX entry)
  
• Samuel Müller and Birgit Pfitzmann. Effektives Compliance Management. In digma - Zeitschrift für Datenrecht und Informationssicherheit, 6 (1), pages 36-39, 2006.
  (BibTeX entry) (Schulthess Juristische Medien AG, Zürich)
  
• Samuel Müller and Birgit Pfitzmann. Compliance Management basierend auf Gesetzesformalisierungen - Das REALM-Projekt. In Tagungsband des 9. Internationalen Rechtsinformatik Symposions (IRIS 2006)., 2006.
  (BibTeX entry) (Richard Boorberg Verlag GmbH)
  
• Samuel Müller and Chonawee Supatgiat. Dynamic and Risk-based Compliance Management. IBM Research, Technical Report RZ 3656, 2006.
  (abstract) (BibTeX entry)
  
• Rolf Oppliger and Ralf Hauser and David Basin. Browser Enhancements to Support SSL/TLS Session-Aware User Authentication. In W3C Workshop on Transparency and Usability of Web Authentication.Proceedings of the World Wide Web Consortium (W3C), 2006.
  (BibTeX entry) (PDF) (Copyright W3C)
  
• Rolf Oppliger and Ralf Hauser and David Basin. SSL/TLS session-aware user authentication - Or how to effectively thwart the man-in-the-middle. In Computer Communications, 29, pages 2238-2246, 2006.
  (BibTeX entry)
  
• Alexander Pretschner. Zur Kosteneffektivitaet des modellbasierten Testens. In Dagstuhl Workshop Modellbasierte Entwicklung eingebetteter Systeme. Technische Universitaet Braunschweig, 2006.
  (BibTeX entry)
  
• Alexander Pretschner and Manuel Hilty and David Basin. Distributed Usage Control. In Communications of the ACM, 49 (9), pages 39-44, 2006.
  (BibTeX entry) ((c) ACM, 2006. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Communications of the ACM 49(9):39-44, September 2006)
  
• Alexander Pretschner and Wolfgang Prenninger. Computing Refactorings of State Machines. In J. Software Systems Modeling, 2006.
  to appear.
  (BibTeX entry)
  
• M. Rappl and A. Pretschner and C. Salzmann and T. Stauner. 3rd International Workshop on Software Engineering for Automotive Systems - SEAS 2006. In 28th Intl. Conf. on Software Engineering (ICSE'06).ACM, 2006.
  (BibTeX entry)
  
• Paul E. Sevinç and David Basin. Controlling Access to Documents: A Formal Access Control Model. ETH Zurich, Technical Report 517, 2006.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Paul E. Sevinç and David Basin and Ernst-Rüdiger Olderog. Controlling Access to Documents: A Formal Access Control Model. In ETRICS 2006.LNCS, 3995. Springer-Verlag, 2006.
  (BibTeX entry) (URL)
  
• Christoph Sprenger and Michael Backes and David Basin and Birgit Pfitzmann and Michael Waidner. Cryptographically Sound Theorem Proving. In 19th IEEE Computer Security Foundations Workshop, Venice, Italy.IEEE Computer Society, 2006.
  (abstract) (BibTeX entry) (PDF)
  
• Christoph Sprenger and Michael Backes and David Basin and Birgit Pfitzmann and Michael Waidner. Cryptographically Sound Theorem Proving. Cryptology ePrint Archive, Technical Report 2006/047, 2006.
  (BibTeX entry) (URL)
  
• M. Utting and A. Pretschner and B. Legeard. A taxonomy of model-based testing. Department of Computer Science, The Universiy of Waikato (New Zealand), Technical Report 04/2006, 2006.
  (BibTeX entry) (URL)
  
• Luca Viganò. Automated Security Protocol Analysis With the AVISPA Tool. In Electronic Notes in Theoretical Computer Science (Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, MFPS XXI), 155, pages 61-86, 2006.
  (BibTeX entry) (http://www.sciencedirect.com)
  
• Michael Wahler and Jana Koehler and Achim D. Brucker. Model-Driven Constraint Engineering. In Workshop on OCL for (Meta-)Models in Multiple Application Domains at the UML/MoDELS Conference., 2006.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Alessandro Armando and David Basin and Jorge Cuellar and Michaël Rusinowitch and Luca Viganò. Special Issue of the Journal of Automated Reasoning on Automated Reasoning for Security Protocol Analysis, volume 36, numbers 1 and 2. In Springer Netherlands, 2006.
  (BibTeX entry)
  
• Pierpaolo Degano and Luca Viganò. Special Issue of Theoretical Computer Science on Automated Reasoning for Security Protocol Analysis, volume 367, numbers 1 and 2. In Elsevier Science, 2006.
  (BibTeX entry)
  
• Pierpaolo Degano and Luca Viganò. Special Issue of the International Journal of Information Security on Automated Reasoning for Security Protocol Analysis. In Springer, 2006.
  In print
  (BibTeX entry)
  
• Manuel Núñez García and Klaus Havelund and Grigore Rosu and Burkhart Wolff. Proceedings of the International Workshop on Formal Aspects of Testing and Runtime Verification (FATES/RV). In Springer Verlag, 2006.
  LNCS 4262.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  
• M. Rappl and A. Pretschner and C. Salzmann and T. Stauner. Proceedings of the 2006 international workshop on Software engineering for automotive systems. In ACM, 2006.
  ISBN:1-59593-402-2
  (BibTeX entry)
  

2005

• E. Abraham and B. Becker and F. Klaedtke and M. Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems. In 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005)., 3385. Springer-Verlag, 2005.
  (BibTeX entry) (Springer-Verlag)
  
• Alessandro Armando and David Basin and Yohan Boichut and Yannick Chevalier and Luca Compagna and Jorge Cuellar and Paul Hankes Drielsma and Pierre-Cyrille Heám and Olga Kouchnarenko and Jacopo Mantovani and Sebastian Mödersheim and von Oheimb, David and Michael Rusinowitch and Judson Santiago and Mathieu Turuani and Luca Viganò and Laurent Vigneron. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Proceedings of CAV'2005. LNCS 3576 Springer-Verlag, 2005.
  (abstract) (BibTeX entry) (PDF) (Springer-Verlag Springer-Verlag)
  
• Alessandro Armando and Luca Viganò. Preface (Editorial). In Electronic Notes in Theoretical Computer Science (Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2004), 125 (1), pages 1, 2005.
  (BibTeX entry) (http://www.sciencedirect.com)
  
• David Aspinall and Christoph Lüth and Burkhart Wolff. Assisted Proof Document Authoring. In Fourth International Conference on Mathematical Knowledge Management (MKM 05). LNCS 3863. Springer Verlag, 2005.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  
• David Basin and Martin Buchheit and Jürgen Doser and Bernhard Hollunder and Torsten Lodderstedt. Model Driven Security. In DACH Security 2005.Syssec Verlag, 2005.
  (BibTeX entry) (PDF)
  
• David Basin and Jürgen Doser and Torsten Lodderstedt. Model Driven Security. Springer, 2005.
  (abstract) (BibTeX entry) (PDF) (© Springer. Ein Unternehmen von Springer Science+Business Media)
  
• David Basin and Hironobu Kuruma and Kazuo Takaragi and Burkhart Wolff. Specifying and Verifying Hysteresis Signature System with HOL-Z. Computer Security Group, ETH Zürich, Technical Report 471, 2005.
  (abstract) (BibTeX entry) (PDF)
  
• David Basin and Hironobu Kuruma and Kazuo Takaragi and Burkhart Wolff. Verification of a Signature Architecture with HOL-Z. In Formal Methods 2005. LNCS 3582 Springer Verlag, 2005.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. Algebraic Intruder Deductions (Extended Version). ETH Zürich, Computer Science, Technical Report 485, 2005.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. Algebraic Intruder Deductions. In LPAR 2005.LNAI, 3835. Springer-Verlag, 2005.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  

• M. Broy and B. Jonsson and J.-P. Katoen and M. Leucker and A. Pretschner Model-Based Testing of Reactive Systems. Springer, 2005. (BibTeX entry) (URL)

  
  
• Achim D. Brucker and Burkhart Wolff. A Verification Approach for Applied System Security. In International Journal on Software Tools for Technology Transfer (STTT), 7 (3), pages 233-247, 2005.
  (abstract) (BibTeX entry) (PDF) (doi:10.1007/s10009-004-0176-3) (© Springer-Verlag)
  
• Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Formal Approaches to Testing of Software (FATES 04). LNCS 3395 Springer-Verlag, 2005.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  
• Achim D. Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 User Guide. Computer Security Group, ETH Zürich, Technical Report 482, 2005.
  (BibTeX entry)
  
• Achim D. Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Formal Approaches to Testing of Software (FATES 05). LNCS 3997 Springer-Verlag, 2005.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  

• Alan Bundy and David Basin and Dieter Hutter and Andrew Ireland Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, 2005. (abstract) (BibTeX entry) (URL) (PDF) (© Cambridge University Press 2005)

  
  
• Carlos Caleiro and Luca Viganò and David Basin. Metareasoning about Security Protocols using Distributed Temporal Logic. In Electronic Notes in Theoretical Computer Science (Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2004), 125 (1), pages 67-89, 2005.
  (BibTeX entry) (http://www.sciencedirect.com)
  
• Carlos Caleiro and Luca Viganò and David Basin. Deconstructing Alice and Bob. In Electronic Notes in Theoretical Computer Science (Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2005), 135 (1), pages 3-22, 2005.
  (BibTeX entry) (Elsevier Science Direct)
  
• Carlos Caleiro and Luca Viganò and David Basin. Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis. In Logic Journal of the IGPL, 13 (6), pages 637-663, 2005.
  (abstract) (BibTeX entry) (URL) (http://jigpal.oxfordjournals.org/)
  
• S.-K. Chen and H. Lei and M. Wahler and H. Chang and K. Bhaskaran and J. Frank. A Model Driven XML Transformation Framework for Business Performance Management. In Proceedings of the IEEE Conference on e-Business Engineering.IEEE Computer Society, 2005.
  (BibTeX entry)
  
• Michael Näf und David Basin. Konflikt oder Review - Zwei Ansätze für Labors in angewandter Informationssicherheit. Information Security, Technical Report 497, 2005.
  (BibTeX entry) (PDF)
  
• Michael Näf und David Basin. Konflikt oder Review - Zwei Ansätze für Labors in angewandter Informationssicherheit. In Informatik Spektrum, 5 (28), 2005.
  (BibTeX entry) (Springer)
  
• Pierpaolo Degano and Luca Viganò. Preface (Editorial). In Electronic Notes in Theoretical Computer Science (Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2005), 135 (1), pages 1-2, 2005.
  (BibTeX entry) (Elsevier Science Direct)
  
• Paul Hankes Drielsma and Sebastian Mödersheim and Luca Viganò. A Formalization of Off-Line Guessing for Security Protocol Analysis. In Proceedings of LPAR'04.LNAI, 3452. Springer, 2005.
  (abstract) (BibTeX entry) (URL) (Springer-Verlag Berlin Heidelberg 2005)
  
• Christopher Giblin and Alice Y Liu and Samuel Müller and Birgit Pfitzmann and Xin Zhou. Regulations Expressed As Logical Models (REALM). IBM Research, Technical Report RZ 3616, 2005.
  (abstract) (BibTeX entry) (PDF)
  
• Christopher Giblin and Alice Y Liu and Samuel Müller and Birgit Pfitzmann and Xin Zhou. Regulations Expressed As Logical Models (REALM). In Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems (JURIX 2005).IOS Press, 2005.
  (abstract) (BibTeX entry) (PDF)
  
• Manuel Hilty and David Basin and Alexander Pretschner. On Obligations. In 10th European Symposium on Research in Computer Security (ESORICS 2005).LNCS, 3679. Springer-Verlag, 2005.
  (abstract) (BibTeX entry) (© Springer Verlag)
  
• M. Hilty and A. Pretschner and T. Walter and C. Schaefer. Usage Control Requirements in Mobile and Ubiquitous Computing Applications. DoCoMo Euro-Labs Internal Technical Report, Technical Report I-ST-015, 2005.
  (BibTeX entry)
  
• Dieter Hutter and Heiko Mantel and Ina Schaefer and Axel Schairer. Security of Multiagent Systems: A Case Study on Comparison Shopping. In To appear in Journal of Applied Logic 2005, Elsevier, 2005.
  (BibTeX entry) (http://kisogawa.inf.ethz.ch/WebBIB/publications/Copyright©2005ElsevierB.V.)
  
• Jana Koehler and Rainer Hauser and Shane Sendall and Michael Wahler. Declarative Techniques for Model-Driven Business Process Integration. In IBM Systems Journal, 44 (1), pages 47-65, 2005.
  (BibTeX entry) (PDF)
  
• Boris Köpf and Heiko Mantel. Eliminating Implicit Information Leaks by Transformational Typing and Unification. ETH Zürich, Technical Report 498, 2005.
  (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Boris Köpf and Heiko Mantel. Eliminating Implicit Information Leaks by Transformational Typing and Unification. In Workshop on Formal Aspects in Security and Trust.LNCS, 3866. Springer, 2005.
  (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Heiko Mantel and Axel Schairer. Exploiting Generic Aspects of Security Models in Formal Developments.. In Mechanizing Mathematical Reasoning. LNCS 2605 Springer, 2005.
  (BibTeX entry)
  
• Thomas Meyer and Burkhart Wolff. Tactic-based Optimized Compilation of Functional Programs. In Types for Proofs and Programs (TYPES 2004). LNCS 3839 Springer Verlag, 2005.
  (abstract) (BibTeX entry) (PDF) (© Springer-Verlag)
  
• Kunihiko Miyazaki and David Basin and Hironobu Kuruma and Kazuo Takaragi and Satoru Tezuka. A formal analysis of a digital signature system. In Computer Software - Journal of the Japanese Society for Software Science and Technology, 22 (2), pages 74-84, 2005.
  in Japanese
  (BibTeX entry) (PDF)
  
• Alexander Pretschner. Model-Based Testing in Practice. In Formal Methods 2005.LNCS, 3582. Springer, 2005.
  (BibTeX entry)
  
• A. Pretschner. Model-Based Testing. In ICSE'05., 2005.
  (BibTeX entry)
  
• A. Pretschner and J. Philipps. Methodological Issues in Model-Based Testing. Springer LNCS, 2005.
  (BibTeX entry)
  
• A. Pretschner and W. Prenninger. Computing Refactorings of Behavior Models. In MODELS 2005.LNCSSpringer, 2005.
  (BibTeX entry)
  
• A. Pretschner and W. Prenninger and S. Wagner and C. Kuehnel and M. Baumgartner and B. Sostawa and R. Zoelch and T. Stauner. One Evaluation of Model-Based Testing and its Automation. In ICSE'05., 2005.
  (BibTeX entry)
  
• C. Salzmann and T. Stauner and A. Pretschner. ICSE workshop: Software Engineering for Automotive Systems. In ICSE'05., 2005.
  (BibTeX entry)
  
• Diana Senn and David Basin and Germano Caronni. Firewall Conformance Testing. In TestCom 2005.Lecture Notes in Computer Science, 3502. Springer-Verlag GmbH, 2005.
  (abstract) (BibTeX entry) (URL) (Springer)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. OFMC: A symbolic model checker for security protocols. In International Journal of Information Security, 4 (3), pages 181-208, 2005.
  Published online December 2004
  (abstract) (BibTeX entry) (URL) (PDF) (Springer-Verlag)
  
• Alessandro Armando and Luca Viganò. Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004). In Electronic Notes in Theoretical Computer Science 125 (Elsevier Science Direct), 2005.
  (BibTeX entry) (http://www.sciencedirect.com)
  
• Pierpaolo Degano and Luca Viganò. Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis, ARSPA 2005). In Electronic Notes in Theoretical Computer Science 135 (Elsevier Science Direct), 2005.
  (BibTeX entry) (Elsevier Science Direct)
  
• Serge Autexier and Iliano Cervesato and Heiko Mantel International Journal of Information Security. Springer, 2005.
  (BibTeX entry) (URL)
  
• A. Pretschner and C. Salzmann and T. Stauner. Proceedings of the 2nd Intl. ICSE workshop on Software Engineering for Automotive Systems. In ACM, 2005.
  ISBN 1-59593-128-7
  (BibTeX entry)
  

2004

• V. Alyokhin and B. Elbel and M. Rothfelder and A. Pretschner. Coverage Metrics for Continuous Function Charts. In 15th IEEE Intl. Symp. on Software Reliability Engineering (ISSRE'04).IEEE, 2004.
  (BibTeX entry)
  
• David Basin. Sicher in die Informationsgesellschaft von morgen?. In PIK: Praxis der Informationsverarbeitung und Kommunikation (3), pages 180-182, 2004.
  ZISC
  (abstract) (BibTeX entry) (URL) (gzip'ed Postscript) (Copyright © 2004 K. G. Saur. / Alle Rechte vorbehalten)
  
• David Basin and Manuel Clavel and Josè Meseguer. Reflective Metalogical Frameworks. In ACM Transactions on Computational Logic, 5 (3), pages 528-576, 2004.
  (abstract) (BibTeX entry) (Copyright © 2004 ACM, Inc.)
  
• David Basin and Yves Deville and Pierre Flener and Andreas Hamfelt and Jorgen Fischer Nilsson. Synthesis of Programs in Computational Logic. In Program Development in Computational Logic. LNCS, volume 3049 Springer-Verlag, 2004.
  (BibTeX entry) (gzip'ed Postscript) (© Springer-Verlag)
  
• David Basin and Kunihiko Miyazaki and Kazuo Takaragi. A Formal Analysis of a Digital Signature Architecture. In Integrity and Internal Control in Information Systems, IV. Kluwer Academic Publishers, 2004.
  (abstract) (BibTeX entry) (Kluwer Academic Publishers)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. OFMC: A Symbolic Model-Checker for Security Protocols. ETH Zürich, Computer Science, Technical Report 450, 2004.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. Computer Security Group, ETH Zürich, Technical Report 449, 2004.
  (abstract) (BibTeX entry)
  
• Carlos Caleiro and Luca Viganò and David Basin. Towards a Metalogic for Security Protocol Analysis. In Proceedings of the Workshop on the Combination of Logics: Theory and Applications (Comblog'04). Center for Logic and Computation, Departamento de Matemática, Instituto Superior Técnico, Lisbon, 2004.
  (BibTeX entry)
  
• Paul Hankes Drielsma and Sebastian Mödersheim. The ASW Protocol Revisited: A Unified View. In Automated Reasoning for Security Protocol Analysis (ARSPA).ENTCS, 2004.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Marieke Huisman and Dilian Gurov and Christoph Sprenger and Gennady Chugunov. Checking Abscence of Illicit Applet Interactions: A Case Study. In FASE 04.Springer, 2004.
  Winner of the EASST award for Best Software Science Paper
  (BibTeX entry) (gzip'ed Postscript)
  
• F. Klaedtke. On the Automata Size for Presburger Arithmetic. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004).IEEE Computer Society Press, 2004.
  (BibTeX entry) (IEEE)
  
• Boris Köpf and Heiko Mantel. Eliminating Timing Leaks by Unification (Extended Abstract). In First International Workshop on Programming Language Interference and Dependence.University of Verona, 2004.
  (BibTeX entry)
  
• Christoph Kreitz and Heiko Mantel. A Matrix Characterization for Multiplicative Exponential Linear Logic. In Journal of Automated Reasoning, 32, pages 121-166, 2004.
  (abstract) (BibTeX entry) (Kluwer)
  
• Jochen Küster and Shane Sendall and Michael Wahler. Comparing two Model Transformation Approaches. In UML 2004. Workshop: OCL and Model Driven Engineering., 2004.
  (BibTeX entry) (PDF)
  
• Heiko Mantel and David Sands. Controlled Declassification based on Intransitive Noninterference. In 2nd ASIAN Symposium on Programming Languages and Systems, APLAS 2004.LNCS, 3302. Springer, 2004.
  (BibTeX entry) (Springer)
  
• Paulo Mateus and Am'ilcar Sernadas and Cristina Sernadas and Luca Viganò. Modal sequent calculi labelled with truth values: completeness, duality and analyticity. In Logic Journal of the Interest Group in Pure and Applied Logics (IGPL), 12 (3), pages 227-274, 2004.
  (BibTeX entry) (URL) (Oxford University Press)
  
• W. Prenninger and A. Pretschner. Abstractions for Model-Based Testing. In 2nd Intl. Workshop on Test and Analysis of Component Based Systems., 2004.
  (BibTeX entry)
  
• A. Pretschner. Modellbasiertes Testen. In Modellierung 2004.LNI, 45. GI, 2004.
  (BibTeX entry)
  
• A. Pretschner and H. Lötzbeyer and J. Philipps. Model Based Testing in Incremental System Development. In Journal of Systems and Software, 70 (3), pages 315-329, 2004.
  (abstract) (BibTeX entry) (Elsevier)
  
• A. Pretschner and O. Slotosch and E. Aiglstorfer and S. Kriebel. Model Based Testing for Real-The Inhouse Card Case Study. In Software Tools for Technology Transfer, 5 (2-3), pages 140-157, 2004.
  (abstract) (BibTeX entry) (Springer Springer Springer)
  
• Nicole Rauch and Burkhart Wolff. Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL. ETH Zürich, Technical Report 458, 2004.
  (abstract) (BibTeX entry) (PDF)
  
• C. Salzmann and T. Stauner and A. Pretschner. ICSE workshop: Software Engineering for Automotive Systems. In ICSE 2004.IEEE, 2004.
  (BibTeX entry)
  
• Heiko Mantel and David Sands. Controlled Declassification based on Intransitive Noninterference. Department of Computer Science, Chalmers University of Technology and Göteborg University, Technical Report 2004-06, 2004.
  (BibTeX entry)
  
• Shane Sendall and Rainer Hauser and Jana Koehler and Jochen Küster and Michael Wahler. Understanding Model Transformation by Classification and Formalization. In Conference on Generative Programming and Component Engineering: Software Transformation Systems Workshop., 2004.
  (BibTeX entry) (PDF)
  
• Christoph Sprenger and Dilian Gurov and Marieke Huisman. Compositional Verification for Secure Loading of Smart Card Applets. In Formal Methods and Models for Co-Design (MEMOCODE).IEEE Computer Society, 2004.
  (abstract) (BibTeX entry) (© IEEE Computer Society)
  
• Yannick Chevalier and Luca Compagna and Jorge Cuellar and Paul Hankes Drielsma and Jacopo Mantovani and Sebastian Mödersheim and Laurent Vigneron. A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In Workshop on Specification and Automated Processing of Security Requirements (SAPS 2004). 2004.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  

• Vijay Atluri and Michael Backes and David Basin and Michael Waidner. Conference on Computer and Communications Security. In ACM Press New York, NY, USA, 2004. (abstract) (BibTeX entry) (Copyright © 2004 ACM, Inc.)

  
  

• David Basin and Michaël Rusinowitch. Automated Reasoning: Second International Joint Conference (IJCAR 2004). In Springer-Verlag, 2004. Volume 3097 (abstract) (BibTeX entry) (© Springer-Verlag)

  
  
• A. Pretschner and C. Salzmann and T. Stauner Proceedings of the ICSE 2004 workshop on Software Engineering for Automotive Systems. IEE, 2004.
  (BibTeX entry) (IEE)
  

2003

• Abdelwaheb Ayari and David Basin and Felix Klaedtke. Decision Procedures for Inductive Boolean Functions based on Alternating Automata. In Theoretical Computer Science, 300 (1-3), pages 301-329, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© Elsevier)
  
• David Basin and Jürgen Doser and Torsten Lodderstedt. Model Driven Security for Process-Oriented Systems. In 8th ACM Symposium on Access Control Models and Technologies.ACM Press, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Jürgen Doser and Torsten Lodderstedt. Model Driven Security: from UML Models to Access Control Infrastructures. ETH Zürich, Technical Report 414, 2003.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich and Marek Gawkowski. Bytecode Verification by Model Checking. In Journal of Automated Reasoning, 30 (3-4), pages 399-444, 2003.
  (abstract) (BibTeX entry) (PDF) (Kluwer Academic Publishers)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. An On-The-Fly Model-Checker for Security Protocol Analysis. In Proceedings of Esorics'03. LNCS 2808 Springer-Verlag, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© Springer-Verlag)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols (Extended Abstract). In SPV'03. 2003.
  (abstract) (BibTeX entry) (URL)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. In CCS'03. ACM Press, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (ACM Press)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. An On-The-Fly Model-Checker for Security Protocol Analysis.. ETH Zürich, Computer Science, Technical Report 404, 2003.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• David Basin and Sebastian Mödersheim and Luca Viganò. Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. ETH Zürich, Computer Science, Technical Report 405, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Frank Rittinger and Burkhart Wolff. HOL-Z 2.0: A Proof Environment for Z-Specifications. In Journal of Universal Computer Science, 9 (2), pages 152-172, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© J.UCS)
  
• Achim D. Brucker and Burkhart Wolff. A Case Study of a Formalized Security Architecture. In Eighth International Workshop onFormal Methods for Industrial Critical Systems (FMICS'03)., 80. Elsevier Science Publishers, 2003.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Burkhart Wolff. Using Theory Morphisms for Implementing Formal Methods Tools. In Types 2002, Proceedings of the workshop Types for Proof and Programs. LNCS 2646. Springer-Verlag, 2003.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  
• S. Gauch and J. Chaffee and A. Pretschner. Ontology-Based Personalized Search and Browsing. In J. Web Intelligence and Agent Systems, 1 (3-4), pages 219-234, 2003.
  (BibTeX entry)
  
• G. Hahn and J. Philipps and A. Pretschner and T. Stauner. Prototype-based Tests for Hybrid Reactive Systems. In Proc. 14th IEEE Intl. workshop on Rapid System Prototyping.IEEE, 2003.
  (abstract) (BibTeX entry)
  
• Heiko Mantel. A Uniform Framework for the Formal Specification and Verification of Information Flow Security. Saarland University,2003.
  (BibTeX entry)
  
• Heiko Mantel and Andrei Sabelfeld. A Unifying Approach to the Security of Distributed and Multi-threaded Programs. In Journal of Computer Security, 11 (4), 2003.
  (BibTeX entry)
  
• J. Philipps and A. Pretschner and O. Slotosch and E. Aiglstorfer. Model-Based Test Case Generation for Smart Cards. In Electronic Notes in Theoretical Computer Science, 80, pages 168-182, 2003.
  (abstract) (BibTeX entry)
  
• A. Pretschner. Compositional Generation of MC/DC Integration Test Suites. In Electronic Notes in Theoretical Computer Science, 82 (6), pages 1-11, 2003.
  (abstract) (BibTeX entry)
  
• Nicole Rauch and Burkhart Wolff. Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL. In Electronic Notes in Theoretical Computer Science., 80. Elsevier Science Publishers, 2003.
  (abstract) (BibTeX entry) (PDF)
  
• Anindya Banerjee and Heiko Mantel and David Naumann and Andrei Sabelfeld. Final Report on Seminar 03411: Language-Based Security. Dagstuhl, 2003.
  (BibTeX entry)
  
• Dieter Hutter and Heiko Mantel and Axel Schairer. Informationsflusskontrolle als Grundlage für die Sicherheit von Multiagentensystemen. In Praxis der Informationsverarbeitung und Kommunikation (PIK), 26 (1), pages 39-47, 2003.
  (BibTeX entry)
  

• Michael Backes and David Basin and Michael Waidner. Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering. In ACM Press, 2003. (BibTeX entry) (ACM, Inc.)

  
  
• David Basin and Burkhart Wolff. Theorem Proving in Higher Order Logics, 16th International Conference (TPHOLs 2003). In Springer-Verlag, 2003.
  LNCS 2758.
  (abstract) (BibTeX entry) (© Springer-Verlag)
  

2002

• Rafael Accorsi and David Basin and Luca Viganò. Modal Specifications of Trace-Based Security Properties. In Proceedings of the Second International Workshop on Security of Mobile Multiagent Systems (SEMAS-2002). Research Report University Saarbrücken, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Alessandro Armando and David Basin and Mehdi Bouallagui and Yannick Chevalier and Luca Compagna and Sebastian Mödersheim and Michael Rusinowitch and Mathieu Turuani and Luca Viganò and Laurent Vigneron. The AVISS Security Protocol Analysis Tool. In Computer-Aided Verification CAV'02. Lecture Notes in Computer Science 2404 Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© Springer-Verlag, Heidelberg)
  
• Abdelwaheb Ayari and David Basin. Qubos: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers. In Formal Methods in Computer-Aided Design, Fourth International Conference, FMCAD 2002.Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Abdelwaheb Ayari and David Basin and Felix Klaedtke. Decision Procedures for Inductive Boolean Functions based on Alternating Automata. In Theoretical Computer Science, 2002.
  to appear
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich and Marek Gawkowski and Joachim Posegga. Bytecode Model Checking: An Experimental Analysis. In Model Checking Software, 9th International SPIN Workshop.LNCS, 2318. Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich and Marek Gawkowski. Verified Bytecode Model Checkers. In Theorem Proving in Higher Order Logics (TPHOLs'02).LNCS, 2410. Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© Springer-Verlag, Heidelberg)
  
• David Basin and Frank Rittinger and Luca Viganò. A Formal Analysis of the CORBA Security Service. In ZB 2002: Formal Specification and Development in Z and B. lncs Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© Springer-Verlag)
  
• K. Bender and M. Broy and I. Péter and A. Pretschner and T. Stauner. Model based development of hybrid systems: specification, simulation, test case generation. In Modelling, Analysis, and Design of Hybrid Systems.LNCIS, 279. Springer, 2002.
  (abstract) (BibTeX entry) (Springer)
  
• Achim D. Brucker and Stefan Friedrich and Frank Rittinger and Burkhart Wolff. HOL-Z 2.0: A Proof Environment for Z-Specifications. In FMTOOLS 2002. Technical Report 2002-11, 2002.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Achim D. Brucker and Frank Rittinger and Burkhart Wolff. The CVS-Server Case Study: A Formalized Security Architecture. In FM-TOOLS 2002. Technical Report 2002-11, 2002.
  (abstract) (BibTeX entry) (URL) (PDF)
  
• Achim D. Brucker and Frank Rittinger and Burkhart Wolff. A CVS-Server Security Architecture - Concepts and Formal Analysis. Albert-Ludwigs-Universität Freiburg, Technical Report 182, 2002.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Burkhart Wolff. A Proposal for a Formal OCL Semantics in Isabelle/HOL. In Theorem Proving in Higher Order Logics. lncs 2410, Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (URL) (PDF) (extended) (© Springer-Verlag)
  
• Achim D. Brucker and Burkhart Wolff. HOL-OCL: Experiences, Consequences and Design Choices. In UML 2002: Model Engineering, Concepts and Tools. lncs 2460, Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (URL) (PDF) (© Springer-Verlag)
  
• Torsten Lodderstedt and David Basin and Jürgen Doser. SecureUML: A UML-Based Modeling Language for Model-Driven Security. In The unified modeling language: model engineering, concepts, and tools; 5th international., 2460. Springer, 2002.
  (abstract) (BibTeX entry) (PDF) (© Springer-Verlag)
  
• João Rasga and Amílcar Sernadas and Cristina Sernadas and Luca Viganò. Labelled Deduction over Algebras of Truth-Values. In Frontiers of Combining Systems 4 (Proceedings of FroCoS'2002). LNCS 2309 Springer-Verlag, 2002.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (© Springer-Verlag)
  
• João Rasga and Amílcar Sernadas and Cristina Sernadas and Luca Viganò. Fibring Labelled Deduction Systems. In Journal of Logic and Computation, 12 (3), pages 443-473, 2002.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript) (© Oxford University Press)
  
• B. Schätz and A. Pretschner and F. Huber and J. Philipps. Model-Based Development of Embedded Systems. In Advances in Object-Oriented Information Systems.LNCS, 2426. Springer, 2002.
  (abstract) (BibTeX entry)
  

2001

• Rafael Accorsi and David Basin and Luca Viganò. Towards an awareness-based semantics for security protocol analysis. In Post-CAV Workshop on Logical Aspects of Cryptographic Protocol Verification. Elsevier Science Publishers, 2001.
  Electronic Notes in Theoretical Computer Science 55(1)
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Abdelwaheb Ayari and David Basin. A Higher-order Interpretation of Deductive Tableau. In Journal of Symbolic Computation, 31 (5), pages 487-520, 2001.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Grit Denker. Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis. In Electronic Notes in Theoretical Computer Science., 36. Elsevier Science Publishers, 2001.
  (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Amy Felty. Current Trends in Logical Frameworks and Metalanguages. In Journal of Automated Reasoning, 31 (5), pages 1-2, 2001.
  (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Harald Ganzinger. Automated Complexity Analysis Based on Ordered Resolution. In Journal of the Association of Computing Machinery, 48 (1), pages 70-109, 2001.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Frank Rittinger and Luca Viganò. A Formal Analysis of the CORBA Security Service. Albert-Ludwigs-Universität Freiburg, Technical Report 154, 2001.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Frank Rittinger and Luca Viganò. A Formal Data-Model of the CORBA Security Service. In 8th European Software Engineering Conference (ESEC).ACM Press, 2001.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Burkhart Wolff. Checking OCL Constraints in Distributed Systems Using J2EE/EJB. Albert-Ludwigs-Universität Freiburg, Technical Report 157, 2001.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• Achim D. Brucker and Burkhart Wolff. Testing Distributed Component Based Systems Using UML/OCL. In Informatik 2001.Tagungsband der GI/ÖCG Jahrestagung, 1 (157). , 2001.
  (abstract) (BibTeX entry) (URL) (PDF) (gzip'ed Postscript)
  
• Ian Frank and David Basin. A Theoretical and Empirical Investigation of Search in Imperfect Information Games. In Theoretical Computer Science, 252 (1-2), pages 217-256, 2001.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• Christoph Lüth and Burkhart Wolff. sml_tk: Functional Programming for GUIs - Reference Manual. Albert-Ludwigs-Universität Freiburg, Technical Report 158, 2001.
  (abstract) (BibTeX entry) (PDF)
  
• A. Pretschner. Classical search strategies for test case generation with Constraint Logic Programming. In Proc. Formal Approaches to Testing of Software., 2001.
  (abstract) (BibTeX entry)
  
• A. Pretschner and H. Lötzbeyer and J. Philipps. &Muml;odel Based Testing in Evolutionary Software Development". In Proc. 12th IEEE Intl. Workshop on Rapid System Prototyping.IEEE, 2001.
  (abstract) (BibTeX entry) (IEEE)
  
• A. Pretschner and O. Slotosch and H. Lötzbeyer and E. Aiglstorfer and S. Kriebel. Model Based Testing for Real: The Inhouse Card Case Study. In Proc. 6th Intl. Workshop on Formal Methods for Industrial Critical Systems., 2001.
  (abstract) (BibTeX entry) (PDF)
  
• Burkhart Wolff. Verifying Explicit Substitution Calculi in Binding Structures with Effect Binding. In Workshop on Explicit Substitution Theory and Applications (WESTAPP'01).Logic Group Preprint Series, 210. Department of Philosophy - Utrecht University, 2001.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  

2000

• Penny Anderson and David Basin. Program Development Schemata as Derived Rules. In Journal of Symbolic Computation, 30 (1), pages 5-36, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Abdelwaheb Ayari and David Basin. Bounded Model Construction for Monadic Second-Order Logics. In 12th International Conference on Computer-Aided Verification (CAV'00).Lecture Notes in Computer Science, 1855. Springer-Verlag, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Abdelwaheb Ayari and David Basin and Felix Klaedtke. Decision Procedures for Inductive Boolean Functions based on Alternating Automata. In 12th International Conference on Computer-Aided Verification (CAV'00).Lecture Notes in Computer Science, 1855. Springer-Verlag, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Manuel Clavel and Josè Meseguer. Rewriting Logic as a Metalogical Framework. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS).Lecture Notes in Computer ScienceSpringer-Verlag, 2000.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich. Combining WS1S and HOL. In Frontiers of Combining Systems 2. Research Studies Press/Wiley, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich and Sebastian Mödersheim. B2M: A Semantic Based Tool for BLIF Hardware Descriptions. In Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000.Lecture Notes in Computer Science, 1954. Springer-Verlag, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Luca Viganò. A Recipe for the Complexity Analysis of Non-Classical Logics. In Frontiers of Combining Systems 2 (Proceedings of FroCoS'98). Studies in Logic and Computation Research Studies Press/Wiley, 2000.
  (abstract) (BibTeX entry)
  
• David Basin and Luca Viganò and Burkhart Wolff. Berichte aus den Instituten: Lehrstuhl für Softwaretechnik und Softwareproduktionsumgebung, Freiburg. In PIK (Praxis der Informationsverarbeitung und Kommunikation), 23 (4), pages 248-249, 2000.
  (BibTeX entry) (PDF) (gzip'ed Postscript) (English translation)
  
• Ian Frank and David Basin and Alan Bundy. Combining Knowledge and Search to Solve Single-Suit Bridge. In AAAI-2000.AAAI-Press, 2000.
  (BibTeX entry) (gzip'ed Postscript)
  
• Christoph Lüth and Burkhart Wolff. More about TAS and IsaWin: Tools for Formal Program Development. In Fundamental Approaches to Software Engineering FASE 200. Joint European Conferences on Theory and Practice of Software ETAPS 2000.Lecture Notes in Computer Science, 1783. Springer Verlag, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Christoph Lüth and Burkhart Wolff. TAS - A Generic Window Inference System. In Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000.Lecture Notes in Computer Science, 1869. Springer Verlag, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• T. Meyer and Burkhart Wolff. Correct Code-Generation in a Generic Framework. In TPHOLs 2000: Supplemental Proceedings.OGI Technical Report CSE 00-009, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• Luca Viganò. An O(n log n)-space decision procedure for the relevance logic B⁺. In Studia Logica, 66 (3), pages 385-407, 2000.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript) (Extended version: Technical report No. 140)
  

• Luca Viganò Labelled Non-Classical Logics. Kluwer Academic Publishers, 2000. (abstract) (BibTeX entry) (additional information)

  
  
• G. Wimmel and H. Lötzbeyer and A. Pretschner and O. Slotosch. Specification Based Test Sequence Generation with Propositional Logic. In Software Testing, Validation, and Reliability, 10 (4), pages 229-248, 2000.
  (BibTeX entry) (Wiley)
  

• David Basin and Marcello D'Agostino and Dov M. Gabbay and Seán Matthews and Luca Viganò Labelled Deduction. Kluwer Academic Publishers, 2000. (abstract) (BibTeX entry) (additional information)

  
  

1999

• Abdelwaheb Ayari and David Basin and Stefan Friedrich. Structural and Behavioral Modeling with Monadic Logics. In The Twenty-Ninth IEEE International Symposium on Multiple-Valued Logic.IEEE Computer Society, 1999.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin. Lazy Infinite-State Analysis of Security Protocols. In Secure Networking - CQRE [Secure] '99.Lecture Notes in Computer Science, 1740. Springer-Verlag, 1999.
  (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich. Modeling a Hardware Synthesis Methodology in Isabelle. In Formal Methods in Systems Design, 15 (2), pages 99-122, 1999.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Stefan Friedrich and Joachim Posegga and Harald Vogt. Java Byte Code Verification by Model Checking. In 11th International Conference on Computer-Aided Verification (CAV'99).Lecture Notes in Computer Science, 1633. Springer-Verlag, 1999.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Seán Matthews and Luca Viganò. Modal Logics K, T, K4, S4: Labelled Proof Systems and New Complexity Results. In The Bulletin of Symbolic Logic, 5 (1), pages 91-93, 1999.
  Abstract of a contributed talk at the 1998 European Summer Meeting of the Association for Symbolic Logic, Logic Colloquium'98
  (BibTeX entry)
  
• Ian Frank and David Basin. Strategies Explained. In Proceedings of the Fifth Game Programming Workshop in Japan (GPW-99)., 1999.
  Also available from the Electrotechnical Laboratory, 1-1-4 Umezono, Japan as Technical Report ETL-99-32
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• Christoph Lüth and Burkhart Wolff. Functional Design and Implementation of Graphical User Interfaces for Theorem Provers. In Journal of Functional Programming, 9 (2), pages 167- 189, 1999.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• A. Pretschner and S. Gauch. Ontology Based Personalized Search. In 11th IEEE Intl. Conf. on Tools with Artificial Intelligence.IEEE, 1999.
  (abstract) (BibTeX entry)
  
• X. Zhu and S. Gauch and L. Gerhard and N. Kral and A. Pretschner. Ontology-Based Web Site Mapping for Information Exploration. In 8th Intl. Conf. on Information and Knowledge Management.ACM, 1999.
  (abstract) (BibTeX entry)
  

1998

• David Basin. Logical Framework Based Program Development. In ACM Computing Surveys, 30 (3es), pages 1-4, 1998.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Nils Klarlund. Automata Based Symbolic Reasoning in Hardware Verification. In Formal Methods in Systems Design, 13 (3), pages 255-288, 1998.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Bernd Krieg-Brückner. Formalization of the Development Process. In Algebraic Foundations of System Specification. Springer-Verlag, 1998.
  (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Seán Matthews and Luca Viganò. Labelled Modal Logics: Quantifiers. In Journal of Logic, Language, and Information, 7 (3), pages 237-263, 1998.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Seán Matthews and Luca Viganò. Natural Deduction for Non-Classical Logics. In Studia Logica, 60 (1), pages 119-160, 1998.
  Special issue on Natural Deduction edited by Frank Pfenning and Wilfried Sieg
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Seán Matthews and Luca Viganò. A Modular Presentation of Modal Logics in a Logical Framework. In The Tbilisi Symposium on Logic, Language and Computation: Selected Papers. CSLI Publications, 1998.
  (abstract) (BibTeX entry)
  
• Ian Frank and David Basin. Optimal Play Against Best Defence: Complexity and Heuristics. In Proceedings of The First International Conference of Computers and Games, CG98.Springer, 1998.
  Lecture Notes in Computer Science, 1558
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• Ian Frank and David Basin. Search in Games with Incomplete Information: A Case Study using Bridge Card Play. In Artificial Intelligence, 100, pages 87-123, 1998.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• Ian Frank and David Basin and H. Matsubara. Finding Optimal Strategies for Imperfect Information Games. In Proceedings of AAAI-98., 1998.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• Chritoph Lüth and Einar W. Karlsen and Kolyang and Stefan Westmeier and Burkhart Wolff. HOL-Z in the UniForM-Workbench - a Case Study in Tool Integration for Z. In 11. International Conference of Z Users ZUM'98.LNCS 1493Springer Verlag, 1998.
  (abstract) (BibTeX entry) (gzip'ed Postscript) (doi:10.1007/BFb0056029)
  

1997

• Abdelwaheb Ayari and David Basin and Andreas Podelski. LISA: A Specification Language Based on WS2S. In 11th International Conference of the European Association for Computer Science Logic (CSL '97).LNCS, 1414. Springer-Verlag, 1997.
  (abstract) (BibTeX entry) (gzip'ed Postscript)
  
• David Basin and Seán Matthews and Luca Viganò. Labelled Propositional Modal Logics: Theory and Practice. In Journal of Logic and Computation, 7 (6), pages 685-717, 1997.
  (abstract) (BibTeX entry) (PDF) (gzip'ed Postscript)
  
• David Basin and Seán Matthews and Luca Viganò. A New Method for Bounding the Complexity of Modal Logics. In Computational Logic and Proof Theory (Proceedings of the 5th Kurt Gödel Colloquium, KGC'97). LNCS 1289 Springer-Verlag, 1997.
  (abstract) (BibTeX entry)
  
• David Basin and Seán Matthews and Luca Viganò. Labelled Quantified Modal Logics. In Proceedings of KI'97 (21st German Annual Conference on Artificial Intelligence). LNAI 1303 Springer-Verlag, 1997.
  (abstract) (BibTeX entry)
  
• Luca Viganò. A Framework for Non-Classical Logics. Universität des Saarlandes,1997.
  (abstract) (BibTeX entry)
  

See what our current research is, browse our group's publications database, look at the software we develop, or take a look at current projects.