@inproceedings{KV-icdt15,
address = {Brussels, Belgium},
month = mar,
year = 2015,
volume = 31,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arenas, Marcelo},
acronym = {{ICDT}'15},
booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'15)},
author = {Koutsos, Adrien and Vianu, Victor},
title = {Process-Centric Views of Data-Driven Business Artifacts},
pages = {247-264},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-icdt15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-icdt15.pdf},
doi = {10.4230/LIPIcs.ICDT.2015.247},
abstract = {Declarative, data-aware workflow models are becoming
increasingly pervasive. While these have numerous benefits, classical
process-centric specifications retain certain advantages. Workflow
designers are used to development tools such as BPMN or UML diagrams, that
focus on control flow. Views describing valid sequences of tasks are also
useful to provide stake-holders with high-level descriptions of the
workflow, stripped of the accompanying data. In this paper we study the
problem of recovering process-centric views from declarative, data-aware
workflow specifications in a variant of IBM's business artifact model. We
focus on the simplest and most natural process-centric views, specified by
finite-state transition systems, and describing regular languages. The
results characterize when process-centric views of artifact systems are
regular, using both linear and branching-time semantics. We also study the
impact of data dependencies on regularity of the views.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{CK-csf17,
address = {Santa Barbara, California, USA},
month = aug,
publisher = {{IEEE} Computer Society Press},
editor = {K{\"o}pf, Boris and Chong, Steve},
acronym = {{CSF}'17},
booktitle = {{P}roceedings of the
30th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'17)},
author = {Comon, Hubert and Koutsos, Adrien},
title = {Formal Computational Unlinkability Proofs of RFID Protocols},
pages = {100-114},
year = {2017},
doi = {10.1109/CSF.2017.9},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CK-csf17.pdf},
url = {http://ieeexplore.ieee.org/document/8049714/},
abstract = {We set up a framework for the formal proofs of
RFID protocols in the computational model. We rely on the
so-called computationally complete symbolic attacker model. Our
contributions are:
1) To design (and prove sound) axioms reflecting the proper-
ties of hash functions (Collision-Resistance, PRF).
2) To formalize computational unlinkability in the model.
3) To illustrate the method, providing the first formal proofs
of unlinkability of RFID protocols, in the computational
model.}
}
@inproceedings{CGKM-csf17,
address = {Santa Barbara, California, USA},
month = aug,
publisher = {{IEEE} Computer Society Press},
editor = {K{\"o}pf, Boris and Chong, Steve},
acronym = {{CSF}'17},
booktitle = {{P}roceedings of the
30th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'17)},
author = {Calzavara, Stefano and Grishchenko, Ilya and Koutsos, Adrien and Maffei, Matteo},
title = {A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications},
pages = {22-36},
year = {2017},
doi = {10.1109/CSF.2017.19},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGKM-csf17.pdf},
url = {http://ieeexplore.ieee.org/document/8049649/},
abstract = {The present paper proposes the first static analysis
for Android applications which is both flow-sensitive on the heap
abstraction and provably sound with respect to a rich formal
model of the Android platform. We formulate the analysis as a
set of Horn clauses defining a sound over-approximation of the
semantics of the Android application to analyse, borrowing ideas
from recency abstraction and extending them to our concurrent
setting. Moreover, we implement the analysis in HornDroid, a
state-of-the-art information flow analyser for Android applica-
tions. Our extension allows HornDroid to perform strong updates
on heap-allocated data structures, thus significantly increasing its
precision, without sacrificing its soundness guarantees. We test
our implementation on DroidBench, a popular benchmark of
Android applications developed by the research community, and
we show that our changes to HornDroid lead to an improvement
in the precision of the tool, while having only a moderate cost in
terms of efficiency. Finally, we assess the scalability of our tool
to the analysis of real applications.}
}
@article{KV-jcss17,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Koutsos, Adrien and Vianu, Victor},
title = {{Process-centric views of data-driven business artifacts}},
volume = {86},
number = {1},
year = {2017},
pages = {82-107},
doi = {10.1016/j.jcss.2016.11.012},
month = jun,
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-jcss17.pdf},
url = {http://dx.doi.org/10.1016/j.jcss.2016.11.012},
abstract = {Declarative, data-aware workflow models are becoming increasingly pervasive. While these have numerous benefits, classical process-centric specifications retain certain advantages. Workflow designers are used to development tools such as BPMN or UML diagrams, that focus on control flow. Views describing valid sequences of tasks are also useful to provide stakeholders with high-level descriptions of the workflow, stripped of the accompanying data. In this paper we study the problem of recovering process-centric views from declarative, data-aware workflow specifications in a variant of IBM's business artifact model. We focus on the simplest process-centric views, specified by finite-state transition systems, describing regular languages. The results characterize when process-centric views of artifact systems are regular, using both linear and branching-time semantics. We also study the impact of data dependencies on regularity of the views. As a side effect, we obtain several new results on verification of business artifacts, including a decidability result for branching-time properties.}
}
@inproceedings{K-csf19,
address = {Hoboken, NJ, USA},
month = jul,
publisher = {{IEEE} Computer Society Press},
editor = {Delaune, St{\'e}phanie and Jia, Limin},
acronym = {{CSF}'19},
booktitle = {{P}roceedings of the
32nd {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'19)},
author = {Adrien Koutsos},
title = {Decidability of a Sound Set of Inference Rules for Computational Indistinguishability},
pages = {48-61},
year = 2019,
doi = {10.1109/CSF.2019.00011},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/K-csf19.pdf},
abstract = {Computational indistinguishability is a key property in cryptography and verification of security protocols. Current tools for proving it rely on cryptographic game transformations. We follow Bana and Comon's approach, axiomatizing what an adversary cannot distinguish. We prove the decidability of a set of first-order axioms which are computationally sound, though incomplete, for protocols with a bounded number of sessions whose security is based on an IND-CCA_2 encryption scheme. Alternatively, our result can be viewed as the decidability of a family of cryptographic game transformations. Our proof relies on term rewriting and automated deduction techniques.}
}
@inproceedings{K-eurosp19,
address = {Stockholm, Sweden},
month = jun,
publisher = {{IEEE} Press},
editor = {Frank Piessens and Frank Stajano},
acronym = {{EuroS\&P}'19},
booktitle = {{P}roceedings of the 4th IEEE European Symposium on
Security and Privacy ({EuroS\&P}'19)},
author = {Adrien Koutsos},
title = {The {5G-AKA} Authentication Protocol Privacy},
pages = {464-479},
year = 2019,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/K-eurosp19.pdf},
doi = {10.1109/EuroSP.2019.00041},
abstract = {We study the 5G-AKA authentication protocol described in the 5G mobile communication standards. This version of AKA tries to achieve a better privacy than the 3G and 4G versions through the use of asymmetric randomized encryption. Nonetheless, we show that except for the IMSI-catcher attack, all known attacks against 5G-AKA privacy still apply. Next, we modify the 5G-AKA protocol to prevent these attacks, while satisfying 5G-AKA efficiency constraints as much as possible. We then formally prove that our protocol is sigma-unlinkable. This is a new security notion, which allows for a fine-grained quantification of a protocol privacy. Our security proof is carried out in the Bana-Comon indistinguishability logic. We also prove mutual authentication as a secondary result.}
}
@inproceedings{BDJKM-csl21,
address = {online},
month = may,
publisher = {{IEEE} Press},
editor = {Alina Oprea and Thorsten Holz},
acronym = {{S\&P}'21},
booktitle = {{P}roceedings of the 42nd IEEE Symposium on Security and Privacy
({S\&P}'21)},
author = {Baelde, David and Delaune, St{\'e}phanie and Jacomme, Charlie and
Koutsos, Adrien and Moreau, Sol{\`e}ne},
title = {An {I}nteractive {P}rover for {P}rotocol {V}erification in the {C}omputational {M}odel},
year = {2021},
pdf = {https://hal.archives-ouvertes.fr/hal-03172119},
url = {https://hal.archives-ouvertes.fr/hal-03172119},
note = {To appear}
}
@phdthesis{koutsos-phd2019,
author = {Adrien Koutsos},
title = {Preuves symboliques de propri{\'e}t{\'e}s d'indistinguabilit{\'e} calculatoire},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = sep,
url = {https://tel.archives-ouvertes.fr/tel-02317745},
pdf = {https://tel.archives-ouvertes.fr/tel-02317745/document}
}
This file was generated by bibtex2html 1.98.