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)
[Download BibTex (BIB, 1012 Bytes) | external page DOI] - 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
[Download BibTex (BIB, 682 Bytes) | Download PDF (PDF, 384 KB) | external page DOI] - Andreas Lochbihler and Alexandra Maximova
Stream Fusion in HOL with Code Generation
In Archive of Formal Proofs, 2014 formal proof development
[Download BibTex (BIB, 356 Bytes) | external page URL] - 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
[Download BibTex (BIB, 531 Bytes) | Download PDF (PDF, 675 KB) | external page DOI] - 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
[Download BibTex (BIB, 655 Bytes) | Download PDF (PDF, 649 KB) | external page DOI] - 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
[Download BibTex (BIB, 572 Bytes) | Download PDF (PDF, 781 KB) | external page DOI] - 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
[Download BibTex (BIB, 361 Bytes) | external page DOI] - 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.
[Download BibTex (BIB, 370 Bytes) | Download PDF (PDF, 402 KB) | external page DOI] - 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.
[Download BibTex (BIB, 445 Bytes) | Download PDF (PDF, 279 KB) | external page DOI] - Florian Haftmann, Andreas Lochbihler, and Wolfgang Schreiner
Towards abstract and executable multivariate polynomials in Isabelle
In: Isabelle Workshop 2014.
[Download BibTex (BIB, 319 Bytes) | Download PDF (PDF, 292 KB)] - Andreas Lochbihler and Marc Züst
Programming TLS in Isabelle/HOL
In: Isabelle Workshop 2014.
[Download BibTex (BIB, 269 Bytes) | Download PDF (PDF, 441 KB)] - 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
[Download BibTex (BIB, 557 Bytes) | Download PDF (PDF, 342 KB) | external page DOI] - 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
[Download BibTex (BIB, 507 Bytes) | external page DOI] - 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
[Download BibTex (BIB, 358 Bytes) | external page DOI] - 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.
[Download BibTex (BIB, 480 Bytes) | Download PDF (PDF, 934 KB) | external page DOI] - 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.
[Download BibTex (BIB, 811 Bytes) | Download PDF (PDF, 340 KB) | external page DOI] - 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.
[Download BibTex (BIB, 536 Bytes) | Download PDF (PDF, 3.3 MB) | Download Technical Report (52 KB) | external page DOI] - Marco Guarnieri and David Basin
Optimal Security-Aware Query Processing
In Proceedings of the VLDB Endowment, Volume 7, Issue 12
[Download BibTex (BIB, 365 Bytes) | Download PDF (PDF, 602 KB) | external page URL] - 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
[Download BibTex (BIB, 648 Bytes) | Download PDF (PDF, 297 KB) | external page DOI] - Ognjen Marić, Christoph Sprenger
Verification of a Transactional Memory Manager under Hardware Failures and Restarts
In Proceedings of FM 2014
Springer, May 2014
[Download BibTex (BIB, 324 Bytes) | Download PDF (PDF, 416 KB) | external page DOI] - Joel Reardon, David Basin, and Srdjan Capkun
On Secure Data Deletion
In the IEEE Security & Privacy Magazine, IEEE, May 2014.
[Download BibTex (BIB, 356 Bytes) | Download PDF (757 KB) | external page DOI] - 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.
[Download BibTex (BIB, 758 Bytes) | Download PDF (PDF, 247 KB) | external page DOI] - 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.
[Download BibTex (BIB, 331 Bytes) | Download PDF (PDF, 234 KB) | external page DOI] - Andreas Lochbihler
Analysing Java's safety guarantees under concurrency
In it - Information Technology, 56(2):82-86,
de Gruyter, 2014.
[Download BibTex (BIB, 306 Bytes) | external page DOI] - Thai Son Hoang
Reasoning about Almost-Certain Convergence Properties Using Event-B
In Science of Computer Programming, 81:108-121,
Elsevier, February 2014.
[Download BibTex (BIB, 396 Bytes) | external page DOI] - 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.
[Download BibTex (BIB, 513 Bytes) | external page DOI] - 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.
[Download BibTex (BIB, 565 Bytes) | Download PDF (PDF, 656 KB)] - 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 page DOI] - 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
[Download BibTex (BIB, 4 KB) | Download PDF (PDF, 374 KB) | external page DOI] - 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
[Download BibTex (BIB, 539 Bytes) | Download PDF (PDF, 374 KB) | external page DOI] - 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
[Download BibTex (BIB, 536 Bytes) | Download PDF (PDF, 318 KB) | external page DOI] - 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
[Download BibTex (BIB, 624 Bytes) | Download PDF (PDF, 338 KB) | external page DOI] - 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
[Download BibTex (BIB, 399 Bytes) | external page DOI]