Publications 2014

Main content

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