Publications 2008

Main content

  • 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 (TXT, 1 KB) | 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
    [abstract (TXT, 1 KB) | BibTeX (TXT, 1 KB) | PDF (PDF, 230 KB) | 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.
    [abstract (TXT, 2 KB) | BibTeX (TXT, 2 KB) | 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.
    [abstract (TXT, 1 KB) | 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.
    [abstract (TXT, 1 KB) | BibTeX (TXT, 2 KB) | 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 (TXT, 619 Bytes) | 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.
    [abstract (TXT, 1 KB) | BibTeX (TXT, 2 KB) | PDF (PDF, 563 KB) | 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.
    [abstract (TXT, 726 Bytes) | BibTeX (TXT, 1 KB) | PDF (PDF, 560 KB) | 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.
    [abstract (TXT, 993 Bytes) | BibTeX (TXT, 1 KB) | 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.
    [abstract (TXT, 728 Bytes) | BibTeX (TXT, 1 KB) | 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.
    [abstract (TXT, 993 Bytes) | BibTeX (TXT, 1 KB) | PDF (PDF, 520 KB) | 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)
    [abstract (TXT, 1 KB) | BibTeX (TXT, 2 KB) | PDF (PDF, 1020 KB) | 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.
    [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
    [BibTeX (TXT, 469 Bytes)]
  • Cas Cremers.
    On the Protocol Composition Logic PCL.
    In ASIACCS'08.ACM, 2008.
    [BibTeX (TXT, 625 Bytes) | 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.
    [BibTeX (TXT, 903 Bytes) | 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.
    [abstract (TXT, 766 Bytes) | BibTeX (TXT, 1010 Bytes) | DOI]
  • Cas J.F. Cremers.
    Session-state reveal is stronger than Ephemeral-key reveal: Breaking the NAXOS protocol.
    2008
    [abstract (TXT, 889 Bytes) | BibTeX (TXT, 1 KB) | 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 | 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 (TXT, 922 Bytes) | BibTeX (TXT, 1 KB) | PDF (PDF, 232 KB) | 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.
    [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.
    [BibTeX (TXT, 437 Bytes) | 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.
    [abstract (TXT, 1 KB) | BibTeX (TXT, 2 KB) | PDF (PDF, 186 KB) | 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.
    [abstract (TXT, 1 KB) | BibTeX (TXT, 2 KB) | PDF (PDF, 602 KB) | 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.
    [BibTeX (TXT, 444 Bytes) | 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.
    [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.
    [BibTeX (TXT, 576 Bytes) | PDF (PDF, 232 KB) | 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.
    [abstract (TXT, 1 KB) | 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.
    [BibTeX (TXT, 907 Bytes) | URL]
  • Felix Klaedtke.
    Bounds on the Automata Size for Presburger Arithmetic.
    In ACM Transactions on Computational Logic, 9 (2), 2008.
    [BibTeX (TXT, 367 Bytes) | 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.
    [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.
    [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.
    [BibTeX (TXT, 408 Bytes) | 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.
    [BibTeX (TXT, 693 Bytes) | DOI]
  • Simona Orzan and Mohammad Torabi Dashti.
    Data Failures.
    In Distributed Computing (DISC '08).LNCS, 5218. Springer, 2008.
    [BibTeX (TXT, 432 Bytes) | 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.
    [abstract (TXT, 1 KB) | BibTeX (TXT, 2 KB) | DOI]
  • Alexander Pretschner.
    Doctoral Symposium.
    In MODELS 2008.Springer, 2008.
    [BibTeX (TXT, 262 Bytes)]
  • A. Pretschner and R. Breu.
    Doktorandensymposium bei der Modellierung 2008.
    In Modellierung 2008. GI, 2008.
    [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.
    [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.
    [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.
    [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.
    [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.
    [BibTeX (TXT, 502 Bytes) | 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.
    [abstract (TXT, 930 Bytes) | BibTeX (TXT, 2 KB) | DOI]
  • Christoph Sprenger and David Basin.
    Cryptographically-sound Protocol-Model Abstractions.
    In Logic in Computer Science (LICS 08)., 0. IEEE Computer Society, 2008.
    [abstract (TXT, 932 Bytes) | BibTeX (TXT, 2 KB) | DOI]
  • Michael Wahler.
    A Pattern Approach to Increasing the Maturity Level of Class Models.
    Idea Group, 2008.
    [BibTeX (TXT, 483 Bytes)]
  • Michael Wahler.
    Using Patterns to Develop Consistent Design Constraints.
    ETH Zurich,2008.
    [abstract (TXT, 2 KB) | BibTeX (TXT, 2 KB) | 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.
    [Bib (BIB, 1 KB) | DOI]
 
 
Page URL: http://www.infsec.ethz.ch/research/publications/pub2008.html
Fri Mar 31 00:40:58 CEST 2017
© 2017 Eidgenössische Technische Hochschule Zürich