Publications 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 1 KB)] - 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.
[Download BibTeX (TXT, 466 Bytes) | external page DOI] - 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.
[Download abstract (TXT, 996 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 257 KB) | external page DOI] - 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.
[Download abstract (TXT, 713 Bytes) | Download BibTeX (TXT, 1 KB) | external page DOI] - 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.
[Download abstract (TXT, 2 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 315 KB) | external page DOI] - David Basin and Ernst-Rüdiger Olderog and Paul E. Sevinç.
Specifying and Analyzing Security Automata using CSP-OZ.
In AsiaCCS 2007.ACM, 2007.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 204 KB) | external page DOI] - Bernd Becker and Christian Dax and Jochen Eisinger and Felix Klaedtke.
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals .
In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Lecture Notes in Computer Science, 4590. Springer-Verlag, 2007.
[Download BibTeX (TXT, 530 Bytes) | external page DOI] - Bernd Becker and Jochen Eisinger and Felix Klaedtke.
Parallelization of Decision Procedures for Automatic Structures.
In 1st Workshop on Omega Automata (OMEGA'07). 2007.
[Download BibTeX (TXT, 328 Bytes)] - Diana von Bidder and David Basin and Germano Caronni.
Midpoints versus Endpoints: From Protocols to Firewalls.
In Applied Cryptography and Network Security (ACNS 2007).
LNCS, 4521. Springer-Verlag, 2007.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 271 KB) | external page DOI] - 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.
[Download BibTeX (TXT, 352 Bytes)] - Achim D. Brucker.
An Interactive Proof Environment for Object-oriented Specifications.
ETH Zurich,2007. ETH Dissertation No. 17097.
[Download abstract (TXT, 967 Bytes) | Download BibTeX (TXT, 3 KB) | Download PDF (PDF, 2.6 MB) | Download gzip'ed Postscript (GZ, 2.2 MB) | URL] - 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.
[Download abstract (TXT, 795 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 263 KB) | Download gzip'ed Postscript (GZ, 248 KB)] - Achim D. Brucker and Jürgen Doser and Burkhart Wolff.
An MDA Framework Supporting OCL.
In Electronic Communications of the EASST, 5, 2007.
[Download abstract (TXT, 819 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 283 KB)]
- 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.
[Download abstract (TXT, 832 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 258 KB)]
- 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 612 KB) | Download gzip'ed Postscript (GZ, 819 KB) | external page DOI]
- Cas Cremers.
Scyther: Unbounded Verification of Security Protocols.
ETH Zurich, Technical Report 572, 2007.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 1 KB) | URL] - Cas Cremers.
Complete Characterization of Security Protocols by Pattern Refinement (Work in Progress).
2007, Dagstuhl Seminar: Formal Protocol Verification Applied
[Download abstract (TXT, 595 Bytes) | Download BibTeX (TXT, 816 Bytes)] - Cas Cremers and Pascal Lafourcade.
Comparing State Spaces in Automatic Security Protocol Verification.
ETH Zurich, Technical Report 558, 2007. Technical report no. 558.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | URL] - Cas Cremers and Pascal Lafourcade.
Comparing State Spaces in Security Protocol Analysis.
In Seventh International Workshop on Automated Verification of Critical Systems.
ENTCS Elsevier ScienceDirect, 2007.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB)] - Christian Dax and Jochen Eisinger and Felix Klaedtke.
Mechanizing the Powerset Construction for Restricted Classes of omega-Automata.
In Proceedings of the 5th International Symposion on Automated Technology for Verification and Analysis (ATVA'07).
Lecture Notes in Computer Science, 4762. Springer-Verlag, 2007.
[Download BibTeX (TXT, 530 Bytes)] - 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.
An intermediate version of this paper is available as ETH technical report no. 528.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 213 KB) | external page DOI] - 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.
[Download abstract (TXT, 2 KB) | Download BibTeX (TXT, 994 Bytes) | Download PDF (PDF, 47 Bytes) | external page DOI] - 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.
[Download abstract (TXT, 529 Bytes) | Download BibTeX (TXT, 901 Bytes)] - 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.
[Download Bib (BIB, 579 Bytes) | external page DOI] - 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.
[Download BibTeX (TXT, 480 Bytes)] - 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.
[Download abstract (TXT, 677 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 291 KB)]
- 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.
[Download abstract (TXT, 2 KB) | Download BibTeX (TXT, 2 KB)] - Simon Meier.
A Formalization of an Operational Semantics of Security Protocols. ETH Zurich, 2007.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 662 KB)] - Sebastian Mödersheim.
Models and Methods for the Automated Analysis of Security Protocols. PhD Thesis, ETH Zürich, 2007.
[Download abstract (TXT, 2 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 1.2 MB) | Download gzip'ed Postscript (PS, 1.8 MB)] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB)] - David Basin and Ernst-Rüdiger Olderog and Paul E. Sevinc.
Specifying and analysing Security Automata using CSP-OZ.
In Information, computer and Communication security, ASIACCS'07.The Association for Computing Machinery, 2007.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | external page DOI]
- 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.
[Download BibTeX (TXT, 391 Bytes)] - Alexander Pretschner and Manuel Hilty and David Basin.
Verteilte Nutzungskontrolle.
In Digma: Zeitschrift fuer Datenrecht und Informationssicherheit, 7 (4), pages 146-149, 2007.
[Download abstract (TXT, 284 Bytes) | Download BibTeX (TXT, 593 Bytes) | Download PDF (PDF, 73 KB)] - 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.
[Download BibTeX (TXT, 422 Bytes)] - 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.
[Download abstract (TXT, 985 Bytes) | Download BibTeX (TXT, 2 KB) | external page DOI] - 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.
[Download abstract (TXT, 1 KB) | Download BibTeX (TXT, 2 KB) | Download PDF (PDF, 236 KB) | external page DOI] - 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.
[Download BibTeX (TXT, 579 Bytes) | Download PDF (PDF, 274 KB) | external page DOI] - 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, IFIP International Federation for Information Processing 2007.
[Download abstract (TXT, 558 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 685 KB) | external page DOI]
- 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.
[Download abstract (TXT, 707 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 255 KB)]
- Michael Wahler and Jana Koehler and Achim D. Brucker.
Model-Driven Constraint Engineering.
In Electronic Communications of the EASST, 5, 2007.
[Download BibTeX (TXT, 440 Bytes) | Download PDF (PDF, 383 KB)] - Makarius Wenzel and Burkhart Wolff.
Building Formal Method Tools in the Isabelle/Isar Framework.
In TPHOLs 2007. LNCS 4732 Springer-Verlag, 2007.
[Download abstract (TXT, 831 Bytes) | Download BibTeX (TXT, 1 KB) | Download PDF (PDF, 230 KB) | external page DOI] - 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.
[Download BibTeX (TXT, 387 Bytes)]