Publications 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB)] - 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
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 230 KB) | external page DOI] - David Basin and Manuel Clavel and Jürgen Doser and Marina Egea.
Automated Analysis of Security-Design Models.
In Information and Software Technology, 2008.
[Download abstract (TXT, 2 KB) | Download BibTeX (TXT, 2 KB) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 1 KB) | 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | external page 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.
[Download BibTeX (TXT, 619 Bytes) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 563 KB) | external page DOI] - Achim D. Brucker and Lukas Brügger and Burkhart Wolff.
Model-based Firewall Conformance Testing.
In Testcom/FATES 2008. LNCS 5047 Springer-Verlag, 2008.
[Download abstract (TXT, 726 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 560 KB) | external page DOI] - 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.
[Download abstract (TXT, 993 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 520 KB)]
- 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.
[Download abstract (TXT, 728 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 426 KB)] - 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.
[Download abstract (TXT, 993 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 520 KB) | external page DOI] - 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)
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 1020 KB) | external page DOI] - 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.
[Download BibTeX (TXT, 381 Bytes)] - 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
[Download BibTeX (TXT, 469 Bytes)] - Cas Cremers.
On the Protocol Composition Logic PCL.
In ASIACCS'08.ACM, 2008.
[Download BibTeX (TXT, 625 Bytes) | external page URL] - 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 Science, Springer-Verlag, 2008.
[Download BibTeX (TXT, 903 Bytes) | external page DOI] - 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.
[Download abstract (TXT, 766 Bytes) | Download BibTeX (TXT, 1010 Bytes) | external page DOI] - Cas J.F. Cremers.
Session-state reveal is stronger than Ephemeral-key reveal: Breaking the NAXOS protocol.
2008
[Download abstract (TXT, 889 Bytes) | Download BibTeX (TXT, 1 KB) | external page 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 | external page 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.
[Download abstract (TXT, 922 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 232 KB) | external page DOI] - 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.
[Download BibTeX (TXT, 359 Bytes)] - 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.
[Download BibTeX (TXT, 437 Bytes) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 186 KB) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 602 KB) | external page DOI] - 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.
[Download BibTeX (TXT, 444 Bytes) | Download PDF (PDF, 179 KB)] - 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.
[Download BibTeX (TXT, 439 Bytes)] - 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.
[Download BibTeX (TXT, 576 Bytes) | Download PDF (PDF, 232 KB) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 1 KB) | 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.
[Download BibTeX (TXT, 907 Bytes) | external page URL] - Felix Klaedtke.
Bounds on the Automata Size for Presburger Arithmetic.
In ACM Transactions on Computational Logic, 9 (2), 2008.
[Download BibTeX (TXT, 367 Bytes) | external page DOI] - 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.
[Download BibTeX (TXT, 445 Bytes)] - 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.
[Download BibTeX (TXT, 367 Bytes)] - Michael Naef and David Basin.
Two approaches to an information security laboratory.
In Communications of the ACM, 51 (12), pages 138-142, 2008.
[Download BibTeX (TXT, 408 Bytes) | external page DOI] - 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.
[Download BibTeX (TXT, 693 Bytes) | external page DOI] - Simona Orzan and Mohammad Torabi Dashti.
Data Failures.
In Distributed Computing (DISC '08).LNCS, 5218. Springer, 2008.
[Download BibTeX (TXT, 432 Bytes) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | external page DOI] - Alexander Pretschner.
Doctoral Symposium.
In MODELS 2008.Springer, 2008.
[Download BibTeX (TXT, 262 Bytes)] - A. Pretschner and R. Breu.
Doktorandensymposium bei der Modellierung 2008.
In Modellierung 2008. GI, 2008.
[Download BibTeX (TXT, 326 Bytes)] - A. Pretschner and M. Hilty and D. Basin and C. Schaefer and T. Walter.
Mechanisms for Usage Control.
In ASIACCS., 2008.
[Download BibTeX (TXT, 292 Bytes)] - 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.
[Download BibTeX (TXT, 413 Bytes)] - 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.
[Download BibTeX (TXT, 341 Bytes)] - A. Pretschner and T. Walter.
Negotiation of Usage Control Policies - Simply the Best.
In 1st Intl. Workshop on Advances in Policy Enforcement., 2008. Keynote.
[Download BibTeX (TXT, 340 Bytes)] - Oppliger Rolf and Hauser Ralf and Basin David.
SSL/TLS Session-Aware User Authentication.
In IEEE Computer, 41 (3), pages 78-84, 2008.
[Download BibTeX (TXT, 502 Bytes) | Download PDF (PDF, 295 KB)] - Christoph Sprenger and David Basin.
Cryptographically-sound Protocol-Model Abstractions.
In Computer Security Foundations (CSF 08)., 0. IEEE Computer Society, 2008.
[Download abstract (TXT, 930 Bytes) | Download BibTeX (TXT, 2 KB) | external page DOI] - Christoph Sprenger and David Basin.
Cryptographically-sound Protocol-Model Abstractions.
In Logic in Computer Science (LICS 08)., 0. IEEE Computer Society, 2008.
[Download abstract (TXT, 932 Bytes) | Download BibTeX (TXT, 2 KB) | external page DOI] - Michael Wahler.
A Pattern Approach to Increasing the Maturity Level of Class Models.
Idea Group, 2008.
[Download BibTeX (TXT, 483 Bytes)] - Michael Wahler.
Using Patterns to Develop Consistent Design Constraints.
ETH Zurich,2008.
[Download abstract (TXT, 2 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 2.9 MB)] - Rolf Oppliger, Ralf Hauser, David Basin
SSL/TLS Session-Aware User Authentication Revisited.
In Computers & Security, 27 (3-5), pages 64-70, 2008.
[Download Bib (BIB, 1 KB) | external page DOI]