Publications 2014
- Gabriel Ciobanu and Thai Son Hoang and Alin Stefanescu
From TiMo to Event-B: Event-Driven Timed Mobility
in Proceedings of the 19th IEEE International Conference on Engineering of Complex Systems (ICECCS 2014)
[DownloadBibTex (BIB, 1012 Bytes)vertical_align_bottom | external pageDOIcall_made] - David Basin, and Cas Cremers
Know Your Enemy: Compromising Adversaries in Protocol Analysis
ACM Transactions on Information and System Security
Vol 17, no. 2, pages 7:1--7:31, November 2014
[DownloadBibTex (BIB, 682 Bytes)vertical_align_bottom | DownloadPDF (PDF, 384 KB)vertical_align_bottom | external pageDOIcall_made] - Andreas Lochbihler and Alexandra Maximova
Stream Fusion in HOL with Code Generation
In Archive of Formal Proofs, 2014 formal proof development
[DownloadBibTex (BIB, 356 Bytes)vertical_align_bottom | external pageURLcall_made] - David Basin, Cas Cremers, Marko Horvat
Actor Key Compromise: Consequences and Countermeasures
in Proceedings of 27th IEEE Computer Security Foundations Symposium (CSF)
Vienna, Austria, 19-22 July 2014
[DownloadBibTex (BIB, 531 Bytes)vertical_align_bottom | DownloadPDF (PDF, 675 KB)vertical_align_bottom | external pageDOIcall_made] - David Basin, Cas Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, and Pawel Szalachowski
ARPKI: Attack Resilient Public-Key Infrastructure
In Proceedings of the ACM Conference on Computer and Communication Security (CCS), 2014
[DownloadBibTex (BIB, 655 Bytes)vertical_align_bottom | DownloadPDF (PDF, 649 KB)vertical_align_bottom | external pageDOIcall_made] - Petar Tsankov, Srdjan Marinovic, Mohammad Torabi Dashti, and David Basin
Fail-Secure Access Control
In Proceedings of the ACM Conference on Computer and Communication Security (CCS), 2014
[DownloadBibTex (BIB, 572 Bytes)vertical_align_bottom | DownloadPDF (PDF, 781 KB)vertical_align_bottom | external pageDOIcall_made] - Barbara Kordy, Sjouke Mauw, Sasa Radomirovic, and Patrick Schweitzer
Attack-defense Trees
In Journal of Logic and Computation
Volume 24, number 1, pages 55-87, 2014
[DownloadBibTex (BIB, 361 Bytes)vertical_align_bottom | external pageDOIcall_made] - Andreas Lochbihler and Johannes Hölzl
Recursive Functions on Lazy Lists via Domains and Topologies
In: Gerwin Klein and Ruben Gamboa (Eds.), Interactive Theorem Proving
LNCS (LNAI) 8558, pp. 341-357, Spriger, 2014.
[DownloadBibTex (BIB, 370 Bytes)vertical_align_bottom | DownloadPDF (PDF, 402 KB)vertical_align_bottom | external pageDOIcall_made] - Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel
Truly Modular (Co)datatypes for Isabelle/HOL
In: Gerwin Klein and Ruben Gamboa (Eds.), Interactive Theorem Proving
LNCS (LNAI) 8558, pp. 93-110, Spriger, 2014.
[DownloadBibTex (BIB, 445 Bytes)vertical_align_bottom | DownloadPDF (PDF, 279 KB)vertical_align_bottom | external pageDOIcall_made] - Florian Haftmann, Andreas Lochbihler, and Wolfgang Schreiner
Towards abstract and executable multivariate polynomials in Isabelle
In: Isabelle Workshop 2014.
[DownloadBibTex (BIB, 319 Bytes)vertical_align_bottom | DownloadPDF (PDF, 292 KB)vertical_align_bottom] - Andreas Lochbihler and Marc Züst
Programming TLS in Isabelle/HOL
In: Isabelle Workshop 2014.
[DownloadBibTex (BIB, 269 Bytes)vertical_align_bottom | DownloadPDF (PDF, 441 KB)vertical_align_bottom] - Miguel Angel García de Dios, Carolina Dania, David Basin, Manuel Clavel
Model-Driven Development of a Secure eHealth Application
in Engineering Secure Future Internet Services and Systems
Volume 8431, series LNCS, pages 97-118
[DownloadBibTex (BIB, 557 Bytes)vertical_align_bottom | DownloadPDF (PDF, 342 KB)vertical_align_bottom | external pageDOIcall_made] - David Basin, Manuel Clavel, Marina Egea, Miguel Angel García de Dios, Carolina Dania
A Model-Driven Methodology for Developing Secure Data-Management Applications
in IEEE Transactions on Software Engineering
Volume 40, number 4, year 2014, pages 324-337
[DownloadBibTex (BIB, 507 Bytes)vertical_align_bottom | external pageDOIcall_made] - David Basin, Samuel J. Burri, Günter Karjoth
Obstruction-free authorization enforcement: Aligning security and business objectives
In Journal of Computer Security
Volume 22, number 5, year 2014, pages 661-698
[DownloadBibTex (BIB, 358 Bytes)vertical_align_bottom | external pageDOIcall_made] - Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin
Automated Verification of Group Key Agreement Protocols
In Proceedings of the 2014 IEEE Symposium on Security and Privacy (S&P)
Pages 179-194, 2014.
[DownloadBibTex (BIB, 480 Bytes)vertical_align_bottom | DownloadPDF (PDF, 934 KB)vertical_align_bottom | external pageDOIcall_made] - Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzini, Peter Y. A. Ryan
Formal Analysis of Electronic Exams
11th International Conference on Security and Cryptography (SECRYPT 2014).
Best Paper Award.
[DownloadBibTex (BIB, 811 Bytes)vertical_align_bottom | DownloadPDF (PDF, 340 KB)vertical_align_bottom | external pageDOIcall_made] - Jannik Dreier, Hugo Jonker, Pascal Lafourcade
Secure Auctions Without Cryptography
In 7th International Conference on Fun with Algorithms (FUN 2014),
volume 8496 of Lecture Notes in Computer Science, pages 158-170, 2014.
[DownloadBibTex (BIB, 536 Bytes)vertical_align_bottom | DownloadPDF (PDF, 3.3 MB)vertical_align_bottom | DownloadTechnical Report (52 KB)vertical_align_bottom | external pageDOIcall_made] - Marco Guarnieri and David Basin
Optimal Security-Aware Query Processing
In Proceedings of the VLDB Endowment, Volume 7, Issue 12
[DownloadBibTex (BIB, 365 Bytes)vertical_align_bottom | DownloadPDF (PDF, 602 KB)vertical_align_bottom | external pageURLcall_made] - Andreas Fürst, Thai Son Hoang, David Basin, Naoto Sato, and Kunihiko Miyazaki
Formal System Modelling Using Abstract Data Types in Event-B
In ABZ, volume 8477 of Lecture Notes in Computer Science, pages 222–237, Toulouse, France,
Springer-Verlag, June 2014
[DownloadBibTex (BIB, 648 Bytes)vertical_align_bottom | DownloadPDF (PDF, 297 KB)vertical_align_bottom | external pageDOIcall_made] - Ognjen Marić, Christoph Sprenger
Verification of a Transactional Memory Manager under Hardware Failures and Restarts
In Proceedings of FM 2014
Springer, May 2014
[DownloadBibTex (BIB, 324 Bytes)vertical_align_bottom | DownloadPDF (PDF, 416 KB)vertical_align_bottom | external pageDOIcall_made] - Joel Reardon, David Basin, and Srdjan Capkun
On Secure Data Deletion
In the IEEE Security & Privacy Magazine, IEEE, May 2014.
[DownloadBibTex (BIB, 356 Bytes)vertical_align_bottom | DownloadPDF (757 KB)vertical_align_bottom | external pageDOIcall_made] - Grgur Petric Maretić, Mohammad Torabi Dashti, and David Basin
Anchored LTL Separation
In the Proceedings of the Twenty-Third EACSL Annual Conference on
Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), ACM, 2014.
[DownloadBibTex (BIB, 758 Bytes)vertical_align_bottom | DownloadPDF (PDF, 247 KB)vertical_align_bottom | external pageDOIcall_made] - Grgur Petric Maretić, Mohammad Torabi Dashti, and David Basin
LTL is Closed Under Topological Closure
In Information Processing Letters, 114:408-413,
Elsevier, May 2014.
[DownloadBibTex (BIB, 331 Bytes)vertical_align_bottom | DownloadPDF (PDF, 234 KB)vertical_align_bottom | external pageDOIcall_made] - Andreas Lochbihler
Analysing Java's safety guarantees under concurrency
In it - Information Technology, 56(2):82-86,
de Gruyter, 2014.
[DownloadBibTex (BIB, 306 Bytes)vertical_align_bottom | external pageDOIcall_made] - Thai Son Hoang
Reasoning about Almost-Certain Convergence Properties Using Event-B
In Science of Computer Programming, 81:108-121,
Elsevier, February 2014.
[DownloadBibTex (BIB, 396 Bytes)vertical_align_bottom | external pageDOIcall_made] - Thai Son Hoang, Annabelle McIver, Larrisa Meinicke, Carroll Morgan, Anthony Sloane, and Enrico Susatyo
Abstractions of Non-interference Security: Probabilistic versus Possibilistic
In Formal Aspects of Computing, 26(1):169-194,
Springer, January 2014.
[DownloadBibTex (BIB, 513 Bytes)vertical_align_bottom | external pageDOIcall_made] - Petar Tsankov, Srdjan Marinovic, Mohammad Torabi Dashti, and David Basin
Decentralized Composite Access Control
In Proceedings of the Third International Conference on Principles of Security and Trust (POST)
Springer, LNCS 8414, pages 245-264, 2014.
[DownloadBibTex (BIB, 565 Bytes)vertical_align_bottom | DownloadPDF (PDF, 656 KB)vertical_align_bottom] - Marco Rocchetto, Martin Ochoa and Mohammad Torabi Dashti
Model-based Detection of CSRF
In the Proceedings of 29th IFIP TC 11 International Conference SEC 2014
Springer, pages 30-43, 2014
[external pageDOIcall_made] - David Basin, Carlos Cotrini Jimenez, Felix Klaedtke, and Eugen Zălinescu
Deciding safety and liveness in TPTL
in Information Processing Letters
Volume 114, issue 12, pages 680–688, 2014
[DownloadBibTex (BIB, 4 KB)vertical_align_bottom | DownloadPDF (PDF, 374 KB)vertical_align_bottom | external pageDOIcall_made] - David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu
On real-time monitoring with imprecise timestamps
in Proceedings of the 5th International Conference on Runtime Verification (RV'2014)
Springer, LNCS 8734, pages 193-198, 2014
[DownloadBibTex (BIB, 539 Bytes)vertical_align_bottom | DownloadPDF (PDF, 374 KB)vertical_align_bottom | external pageDOIcall_made] - David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke and Heiko Mantel
Scalable Offline Monitoring
In Proceedings of the 5th International Conference on Runtime Verification (RV'2014)
Springer, LNCS 8734, pages 31-47, 2014
[DownloadBibTex (BIB, 536 Bytes)vertical_align_bottom | DownloadPDF (PDF, 318 KB)vertical_align_bottom | external pageDOIcall_made] - Andreas Fürst, Thai Son Hoang, David Basin, Krishnaji Desai, Naoto Sato, and Kunihiko Miyazaki
Code Generation for Event-B
In Integrated Formal Methods, volume 8739 of Lecture Notes in Computer Science, pages 323–338, Bertinoro, Italy,
Springer-Verlag, LNCS 0302-9743, pages 323-338, 2014
[DownloadBibTex (BIB, 624 Bytes)vertical_align_bottom | DownloadPDF (PDF, 338 KB)vertical_align_bottom | external pageDOIcall_made] - Stefan Hallerstede, and Thai Son Hoang
Refinement of Decomposed Models by Interface Instantiation
In Science of Computer Programming, 94(2):144-163, November 2014, Elsevier
[DownloadBibTex (BIB, 399 Bytes)vertical_align_bottom | external pageDOIcall_made]