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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom] - 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.
[DownloadBibTeX (TXT, 466 Bytes)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 996 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 257 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 713 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 2 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 315 KB)vertical_align_bottom | external pageDOIcall_made] - David Basin and Ernst-Rüdiger Olderog and Paul E. Sevinç.
Specifying and Analyzing Security Automata using CSP-OZ.
In AsiaCCS 2007.ACM, 2007.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 204 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[DownloadBibTeX (TXT, 530 Bytes)vertical_align_bottom | external pageDOIcall_made] - Bernd Becker and Jochen Eisinger and Felix Klaedtke.
Parallelization of Decision Procedures for Automatic Structures.
In 1st Workshop on Omega Automata (OMEGA'07). 2007.
[DownloadBibTeX (TXT, 328 Bytes)vertical_align_bottom] - 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 271 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[DownloadBibTeX (TXT, 352 Bytes)vertical_align_bottom] - Achim D. Brucker.
An Interactive Proof Environment for Object-oriented Specifications.
ETH Zurich,2007. ETH Dissertation No. 17097.
[Downloadabstract (TXT, 967 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 3 KB)vertical_align_bottom | DownloadPDF (PDF, 2.6 MB)vertical_align_bottom | Downloadgzip'ed Postscript (GZ, 2.2 MB)vertical_align_bottom | 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.
[Downloadabstract (TXT, 795 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 263 KB)vertical_align_bottom | Downloadgzip'ed Postscript (GZ, 248 KB)vertical_align_bottom] - Achim D. Brucker and Jürgen Doser and Burkhart Wolff.
An MDA Framework Supporting OCL.
In Electronic Communications of the EASST, 5, 2007.
[Downloadabstract (TXT, 819 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 283 KB)vertical_align_bottom]
- 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.
[Downloadabstract (TXT, 832 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 258 KB)vertical_align_bottom]
- 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 612 KB)vertical_align_bottom | Downloadgzip'ed Postscript (GZ, 819 KB)vertical_align_bottom | external pageDOIcall_made]
- Cas Cremers.
Scyther: Unbounded Verification of Security Protocols.
ETH Zurich, Technical Report 572, 2007.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | URL] - Cas Cremers.
Complete Characterization of Security Protocols by Pattern Refinement (Work in Progress).
2007, Dagstuhl Seminar: Formal Protocol Verification Applied
[Downloadabstract (TXT, 595 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 816 Bytes)vertical_align_bottom] - Cas Cremers and Pascal Lafourcade.
Comparing State Spaces in Automatic Security Protocol Verification.
ETH Zurich, Technical Report 558, 2007. Technical report no. 558.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom] - 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.
[DownloadBibTeX (TXT, 530 Bytes)vertical_align_bottom] - 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 213 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 2 KB)vertical_align_bottom | DownloadBibTeX (TXT, 994 Bytes)vertical_align_bottom | DownloadPDF (PDF, 47 Bytes)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 529 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 901 Bytes)vertical_align_bottom] - 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.
[DownloadBib (BIB, 579 Bytes)vertical_align_bottom | external pageDOIcall_made] - 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.
[DownloadBibTeX (TXT, 480 Bytes)vertical_align_bottom] - 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.
[Downloadabstract (TXT, 677 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 291 KB)vertical_align_bottom]
- 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.
[Downloadabstract (TXT, 2 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom] - Simon Meier.
A Formalization of an Operational Semantics of Security Protocols. ETH Zurich, 2007.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 662 KB)vertical_align_bottom] - Sebastian Mödersheim.
Models and Methods for the Automated Analysis of Security Protocols. PhD Thesis, ETH Zürich, 2007.
[Downloadabstract (TXT, 2 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 1.2 MB)vertical_align_bottom | Downloadgzip'ed Postscript (PS, 1.8 MB)vertical_align_bottom] - 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom] - 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | external pageDOIcall_made]
- 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.
[DownloadBibTeX (TXT, 391 Bytes)vertical_align_bottom] - Alexander Pretschner and Manuel Hilty and David Basin.
Verteilte Nutzungskontrolle.
In Digma: Zeitschrift fuer Datenrecht und Informationssicherheit, 7 (4), pages 146-149, 2007.
[Downloadabstract (TXT, 284 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 593 Bytes)vertical_align_bottom | DownloadPDF (PDF, 73 KB)vertical_align_bottom] - 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.
[DownloadBibTeX (TXT, 422 Bytes)vertical_align_bottom] - 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.
[Downloadabstract (TXT, 985 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 1 KB)vertical_align_bottom | DownloadBibTeX (TXT, 2 KB)vertical_align_bottom | DownloadPDF (PDF, 236 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[DownloadBibTeX (TXT, 579 Bytes)vertical_align_bottom | DownloadPDF (PDF, 274 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[Downloadabstract (TXT, 558 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 685 KB)vertical_align_bottom | external pageDOIcall_made]
- 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.
[Downloadabstract (TXT, 707 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 255 KB)vertical_align_bottom]
- Michael Wahler and Jana Koehler and Achim D. Brucker.
Model-Driven Constraint Engineering.
In Electronic Communications of the EASST, 5, 2007.
[DownloadBibTeX (TXT, 440 Bytes)vertical_align_bottom | DownloadPDF (PDF, 383 KB)vertical_align_bottom] - Makarius Wenzel and Burkhart Wolff.
Building Formal Method Tools in the Isabelle/Isar Framework.
In TPHOLs 2007. LNCS 4732 Springer-Verlag, 2007.
[Downloadabstract (TXT, 831 Bytes)vertical_align_bottom | DownloadBibTeX (TXT, 1 KB)vertical_align_bottom | DownloadPDF (PDF, 230 KB)vertical_align_bottom | external pageDOIcall_made] - 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.
[DownloadBibTeX (TXT, 387 Bytes)vertical_align_bottom]