@inproceedings{Laf-secret06,
address = {Venice, Italy},
month = jul,
year = 2007,
number = 4,
volume = 171,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Fern{\'a}ndez, Maribel and Kirchner, Claude},
acronym = {{SecReT}'06},
booktitle = {{P}roceedings of the 1st
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'06)},
author = {Lafourcade, Pascal},
title = {Intruder Deduction for the Equational Theory of
{\emph{Exclusive-or}}
with Commutative and Distributive Encryption},
pages = {37-57},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Laf-secret06-long.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Laf-secret06-long.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Laf-secret06-long.ps},
nomorelongpdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2005-21.pdf},
nomorelongps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-21.ps},
nomorelongpsgz = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PSGZ/
rr-lsv-2005-21.ps.gz},
doi = {10.1016/j.entcs.2007.02.054},
abstract = {The first step in the verification of cryptographic protocols is
to decide the intruder deduction problem, that is the vulnerability to a
so-called passive attacker. We~extend the Dolev-Yao model in order to
model this problem in presence of the equational theory of a commutative
encryption operator which distributes over the \emph{exclusive-or}
operator. The~interaction between the commutative distributive law of the
encryption and \emph{exclusive-or} offers more possibilities to decrypt an
encrypted message than in the non-commutative case, which imply a more
careful analysis of the proof system. We~prove decidability of the
intruder deduction problem for a commutative encryption which distributes
over \emph{exclusive-or} with a DOUBLE-EXPTIME procedure. And~we obtain
that this problem is EXPSPACE-hard in the binary case.}
}
@inproceedings{BJ-arspa07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
editor = {Degano, Pierpaolo and K{\"u}sters, Ralf and Vigan{\`o}, Luca and
Zdancewic, Steve},
acronym = {{FCS-ARSPA}'07},
booktitle = {{P}roceedings of the {J}oint {W}orkshop on {F}oundations of
{C}omputer {S}ecurity and {A}utomated {R}easoning
for {S}ecurity {P}rotocol {A}nalysis ({FCS-ARSPA}'07)},
author = {Adel Bouhoula and Florent Jacquemard},
title = {Verifying Regular Trace Properties of Security Protocols
with Explicit Destructors and Implicit Induction},
pages = {27-44},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-arspa07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-arspa07.pdf},
abstract = {We present a procedure for the verification of
cryptographic protocols based on a new method for automatic implicit
induction theorem proving for specifications made of conditional and
constrained rewrite rules. The~method handles axioms between constructor
terms which are used to introduce explicit destructor symbols for the
specification of cryptographic operators. Moreover, it can deal with
non-confluent rewrite systems. This is required in the context of the
verification of security protocols because of the non-deterministic
behavior of attackers. Our~induction method makes an intensive use of
constrained tree grammars, which are used in proofs both as induction
schemes and as oracles for checking validity and redundancy criteria by
reduction to an emptiness problem. The grammars make possible the
development of a generic framework for the specification and verification
of protocols, where the specifications can be parametrized with (possibly
infinite) regular sets of user names or attacker's initial knowledge and
complex security properties can be expressed, referring to some fixed
regular sets of bad traces representing potential vulnerabilities.
We present some case studies giving very promising results, for the detection
of attacks (our~procedure is complete for refutation), and also for the
validation of protocols.}
}
@mastersthesis{chambart-master,
author = {Chambart, Pierre},
title = {Canaux fiables et non-fiables~: fronti{\`e}res de la d{\'e}cidabilit{\'e}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2007,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/chambart-m2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/chambart-m2.pdf}
}
@phdthesis{gascon-these2007,
author = {Gascon, R{\'e}gis},
title = {Sp{\'e}cification et v{\'e}rification de propri{\'e}t{\'e}s
quantitatives sur des automates {\`a} contraintes},
year = 2007,
month = nov,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-RG07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-RG07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-RG07.ps},
futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
these-FC07-slides.pdf}
}
@inproceedings{Bur-nordsec07,
address = {Reykjavik, Iceland},
month = oct,
year = 2007,
editor = {Erlingsson, {\'U}lfar and Sabelfeld, Andrei},
acronym = {{NordSec}'07},
booktitle = {{P}roceedings of the 12th {N}ordic {W}orkshop on {S}ecure {IT}
{S}ystems ({NordSec}'07)},
author = {Bursztein, Elie},
title = {Time has something to tell us about network address
translation},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-nordsec07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-nordsec07.pdf},
abstract = { In this paper we introduce a new technique to count the number
of host behind a~NAT. This technique based on TCP timestamp option, work
with Linux and BSD system and therefore is complementary to the previous
one base on IPID than does not work for those systems. Our~implementation
demonstrates the practicability of this method.}
}
@inproceedings{BE-acsd07,
address = {Bratislava, Slovak Republik},
month = jul,
year = 2007,
publisher = {{IEEE} Computer Society Press},
editor = {Basten, Twan and Shukla, Sandeep},
acronym = {{ACSD}'07},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'07)},
author = {Braunstein, C{\'e}cile and Encrenaz, Emmanuelle},
title = {Using {CTL} formulae as component abstraction in a design and
verification flow},
pages = {80-89},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-acsd07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-acsd07.pdf},
doi = {10.1109/ACSD.2007.76},
abstract = {The verification of global properties (involving several
components) is difficult to achieve, due to combinatorial explosion
problem, while the verification of each component is easier to perform.
Following the idea of~[F.~Xie and J.~Browne. \textit{Verified Systems by
Composition from Verified Components}. In~ESEC/FSE'03, pages~277-286,
Helsinki, Finland, 2003. ACM~Press], we~propose to build an abstraction
of a component already verified, starting from a subset of its
specification described as CTL formulae. This abstraction replaces the
concrete component in the context of global properties verification. }
}
@techreport{Prouve:rap10,
author = {Delaune, St{\'e}phanie and Klay, Francis},
title = {Synth{\`e}se des exp{\'e}rimentations},
institution = {projet RNTL PROUV{\'E}},
month = may,
year = 2007,
type = {Technical Report},
number = 10,
note = {10~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap10.pdf},
abstract = {Dans ce document nous pr{\'e}sentons une synth{\`e}se des deux
cas d'{\'e}tude trait{\'e}s durant le projet. Rappelons qu'il s'agit d'une
part d'un protocole de commerce {\'e}lectronique et d'autre part d'un
protocole de vote. Pour chacun de ces protocoles, nous analysons les
r{\'e}sultats obtenus afin de d{\'e}gager l'apport des travaux issus du
projet et les aspects qui n'ont pas pu etre compl{\`e}tement trait{\'e}s.
Compte tenu des enseignements tir{\'e}s, dans la derni{\`e}re partie nous
mettons en perspectives les axes de recherches envisageables pour traiter
compl{\`e}tement des protocoles aussi complexes que celui du vote
{\'e}lectronique.}
}
@techreport{LSV:07:31,
author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l},
title = {Rewrite Closure of {H}edge-Automata Languages},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = oct,
type = {Research Report},
number = {LSV-07-31},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-31.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-31.pdf},
note = {22~pages},
abstract = {We investigate some preservation properties for classes of
regular languages of unranked ordered terms under an appropriate
generalization of term rewriting subsuming both standard term rewriting
and word rewriting.\par
The considered classes include languages of hedge automata (HA) and some
extension (called CF-HA) with context-free languages in transitions,
instead of regular languages. In~particular, we~show, with a HA completion
procedure, that the set of unranked terms reachable from a given HA
language, using a so called inverse context-free rewrite system, is an HA
language. Moreover, we~prove, using different techniques, the closure of
CF-HA languages with respect to context-free rewrite systems, the
symmetric case of the above rewrite systems. As~a consequence,
the~problems of ground reachability and regular hedge model checking are
decidable in both cases. We~give several several counter examples showing
that we cannot relax the restrictions.}
}
@mastersthesis{dacosta-master,
author = {Da{~}Costa, Arnaud},
title = {Propri{\'e}t{\'e}s de jeux multi-agents},
school = {{M}aster de {L}ogique {M}ath{\'e}matique
et {F}ondements de l'{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2007,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dacosta-m2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dacosta-m2.pdf}
}
@mastersthesis{villard-master,
author = {Villard, Jules},
title = {Logique spatiale pour le pi-calcul appliqu{\'e}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2007,
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-m2.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-m2.pdf}
}
@mastersthesis{vacher-master,
author = {Vacher, Camille},
title = {Accessibilit{\'e} inverse dans les automates d'arbres {\`a}
m{\'e}moire d'ordre sup{\'e}rieur},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = 2007,
month = sep,
oldurl = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-m2.pdf},
oldpdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-m2.pdf},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-35.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-35.pdf}
}
@inproceedings{CL-avocs07,
address = {Oxford, UK},
month = sep,
year = {2007},
editor = {Goldsmith, Michael and Roscoe, Bill},
acronym = {{AVoCS}'07},
booktitle = {{P}re-proceedings of the 7th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'07)},
author = {Cremers, Cas and Lafourcade, Pascal},
title = {Comparing State Spaces in Automatic Security Protocol Verification},
nmnote = {Pas paru dans les proceedings ENTCS},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-avocs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-avocs07.pdf},
abstract = {Many tools exist for automatic security protocol verification,
and most of them have their own particular language for specifying
protocols and properties. Several protocol specification models and
security properties have been already formally related to each other.
However, there is a further difference between verification tools, which
has not been investigated in depth before: the~explored state space. Some
tools explore all possible behaviors, whereas others explore strict
subsets, often by using so-called scenarios. Ignoring such differences can
lead to wrong interpretations of the output of a tool. We~relate the
explored state spaces to each other and find previously unreported
differences between the various approaches. We~apply our study of state
space relations in a performance comparison of several well-known
automatic tools for security protocol verification. We~model a set of
protocols and their properties as homogeneous as possible for each tool.
We~analyze the performance of the tools over comparable state spaces. This
work allows us for the first time to compare these automatic tools fairly,
i.e.,~using the same protocol description and exploring the same state
space. We~also propose some explanations for our experimental results,
leading to a better understanding of the tools.}
}
@inproceedings{BG-asian07,
address = {Doha, Qatar},
month = dec,
year = 2007,
volume = 4846,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cervesato, Iliano},
acronym = {{ASIAN}'07},
booktitle = {{P}roceedings of the 12th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'07)},
author = {Bursztein, Elie and Goubault{-}Larrecq, Jean},
title = {A Logical Framework for Evaluating Network Resilience Against
Faults and Attacks},
pages = {212-227},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf},
doi = {10.1007/978-3-540-76929-3_20},
abstract = {We present a logic-based framework to evaluate the resilience of
computer networks in the face of incidents, i.e., attacks
from malicious intruders as well as random faults. Our model
uses a two-layered presentation of dependencies between
files and services, and of timed games to represent not just
incidents, but also the dynamic responses from
administrators and their respective delays. We demonstrate
that a variant TATL\(\Diamond\) of timed alternating-time temporal
logic is a convenient language to express several desirable
properties of networks, including several forms of
survivability. We illustrate this on a simple redundant Web
service architecture, and show that checking such timed
games against the so-called TATL\(\Diamond\) variant of the timed
alternating time temporal logic TATL is EXPTIME-complete.}
}
@inproceedings{HIRV-atva2007,
address = {Tokyo, Japan},
month = oct,
year = {2007},
volume = 4762,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Namjoshi, Kedar and Yoneda, Tomohiro},
acronym = {{ATVA}'07},
booktitle = {{P}roceedings of the 5th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'07)},
author = {Habermehl, Peter and Iosif, Radu and Rogalewicz, Adam and
Vojnar, Tom{\'a}{\v{s}}},
title = {Proving Termination of Tree Manipulating Programs},
pages = {145-161},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HIRV-atva07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HIRV-atva07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HIRV-atva07.ps},
doi = {10.1007/978-3-540-75596-8_12},
abstract = {We consider the termination problem of programs manipulating
tree-like dynamic data structures. Our~approach is based on a
counter-example guided abstraction refinement loop. We use abstract
regular tree model-checking to infer invariants of the program. Then,
we~translate the program to a counter automaton~(CA) which simulates~it.
If~the CA can be shown to terminate using existing techniques, the~program
terminates. If~not, we analyse the possible counterexample given by a~CA
termination checker and either conclude that the program does not
terminate, or else refine the abstraction and repeat. We~show that the
spuriousness problem for lasso-shaped counterexamples is decidable in some
non-trivial cases. We~applied the method successfully on several
interesting case studies. }
}
@inproceedings{BHJS-fct07,
address = {Budapest, Hungary},
month = aug,
year = 2007,
volume = 4639,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and {\'E}sik, Zolt{\'a}n},
acronym = {{FCT}'07},
booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium
on {F}undamentals of {C}omputation {T}heory
({FCT}'07)},
author = {Bouajjani, Ahmed and Habermehl, Peter and
Jurski, Yan and Sighireanu, Mihaela},
title = {Rewriting Systems with Data~-- {A} Framework for Reasoning About Systems with Unbounded
Structures over Infinite Data Domains},
pages = {1-22},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHJS-fct07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHJS-fct07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHJS-fct07.ps},
doi = {10.1007/978-3-540-74240-1_1},
abstract = {We introduce a uniform framework for reasoning about
infinite-state systems with unbounded control structures and unbounded
data domains. Our~framework is based on constrained rewriting systems on
words over an infinite alphabet. We~consider several rewriting semantics:
factor, prefix, and multiset rewriting. Constraints are expressed in a
logic on such words which is parametrized by a first-order theory on the
considered data domain. We show that our framework is suitable for
reasoning about various classes of systems such as recursive sequential
programs, multithreaded programs, parametrized and dynamic networks of
processes,~etc. Then, we provide generic results (1)~for the decidability
of the satisfiability problem of the fragment of this logic provided that
the underlying logic on data is decidable, and (2)~for proving inductive
invariance and for carrying out Hoare style reasoning within this
fragment. We also show that the reachability problem if decidable for a
class of prefix rewriting systems with integer data.}
}
@inproceedings{GPT-aplas07,
address = {Singapore},
month = nov # {-} # dec,
year = 2007,
volume = 4807,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Shao, Zhong},
acronym = {{APLAS}'07},
booktitle = {{P}roceedings of the 5th {A}sian {S}ymposium
on {P}rogramming {L}anguages and {S}ystems
({APLAS}'07)},
author = {Goubault{-}Larrecq, Jean and Palamidessi, Catuscia and
Troina, Angelo},
title = {A Probabilistic Applied Pi-Calculus},
pages = {175-290},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GPT-aplas07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GPT-aplas07.pdf},
doi = {10.1007/978-3-540-76637-7_12},
abstract = {We propose an extension of the Applied Pi-calculus by
introducing nondeterministic and probabilistic choice operators. The
semantics of the resulting model, in which probability and nondeterminism
are combined, is given by Segala's Probabilistic Automata driven by
schedulers which resolve the nondeterministic choice among the probability
distributions over target states. Notions of static and observational
equivalence are given for the enriched calculus. In order to model the
possible interaction of a process with its surrounding environment a
labeled semantics is given together with a notion of weak bisimulation
which is shown to coincide with the observational equivalence. Finally, we
prove that results in the probabilistic framework are preserved in a
purely nondeterministic setting.}
}
@inproceedings{ABG-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
title = {Automata and Logics for Timed Message Sequence Charts},
pages = {290-302},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABG-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_24},
abstract = {We provide a framework for distributed systems that impose timing constraints
on their executions. We~propose a timed model of communicating finite-state machines,
which communicate by exchanging messages through channels and use event clocks to
generate collections of timed message sequence charts~(T-MSCs). As~a specification
language, we~propose a monadic second-order logic equipped with timing predicates and
interpreted over~T-MSCs. We establish expressive equivalence of our automata and logic.
Moreover, we prove that, for (existentially) bounded channels, emptiness and
satisfiability are decidable for our automata and logic.}
}
@inproceedings{CS-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
title = {{P}ost Embedding Problem is not Primitive Recursive,
with Applications to Channel Systems},
pages = {265-276},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_22},
abstract = {We introduce \textsf{PEP}, the Post Embedding Problem, a variant
of \textsf{PCP} where one compares strings with the subword relation, and
\textsf{PEP}\textsuperscript{reg}, a further variant where solutions are
constrained and must belong to a given regular language.
\textsf{PEP}\textsuperscript{reg} is decidable but not primitive
recursive. This entails the decidability of reachability for
unidirectional systems with one reliable and one lossy channel. }
}
@inproceedings{CDD-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Cortier, V{\'e}ronique and Delaitre, J{\'e}r{\'e}mie and
Delaune, St{\'e}phanie},
title = {Safely Composing Security Protocols},
pages = {352-363},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07.pdf},
addendumpdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
CDD-fsttcs07-addendum.pdf},
doi = {10.1007/978-3-540-77050-3_29},
abstract = {Security protocols are small programs that are executed in
hostile environments. Many results and tools have been developed to
formally analyze the security of a protocol in the presence of active
attackers that may block, intercept and send new messages. However even
when a protocol has been proved secure, there is absolutely no guarantee
if the protocol is executed in an environment where other protocols,
possibly sharing some common identities and keys like public keys or
long-term symmetric keys, are executed.\par
In this paper, we show that security of protocols can be easily composed.
More precisely, we show that whenever a protocol is secure, it remains
secure even in an environment where arbitrary protocols are executed,
provided each encryption contains some tag identifying each protocol, like
e.g.~the name of the protocol.}
}
@inproceedings{BBBBG-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Baier, Christel and Bertrand, Nathalie and Bouyer, Patricia
and Brihaye, {\relax Th}omas and Gr{\"o}{\ss}er, Marcus},
title = {Probabilistic and Topological Semantics for Timed Automata},
pages = {179-191},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
doi = {10.1007/978-3-540-77050-3_15},
abstract = {Like most models used in model-checking, timed automata are an
idealized mathematical model used for representing systems with strong
timing requirements. In~such mathematical models, properties can be
violated, due to unlikely (sequences~of) events. We~propose two new
semantics for the satisfaction of LTL formulas, one based on
probabilities, and the other one based on topology, to rule out these
sequences. We~prove that the two semantics are equivalent and lead to a
PSPACE-Complete model-checking problem for LTL over finite executions.}
}
@inproceedings{BKM-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Bollig, Benedikt and Kuske, Dietrich and Meinecke, Ingmar},
title = {Propositional Dynamic Logic for Message-Passing Systems},
pages = {303-315},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKM-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKM-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BKM-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_25},
abstract = {We examine a bidirectional Propositional Dynamic Logic~(PDL) for message
sequence charts~(MSCs) extending LTL and~TLC\textsuperscript{-}.
Every formula is translated into an equivalent communicating finite-state
machine~(CFM) of exponential size. This synthesis problem is solved in full generality,
i.e.,~also for MSCs with unbounded channels. The model checking problems for CFMs and
for HMSCs against PDL formulas are shown to be in PSPACE for existentially
bounded~MSCs. It~is shown that CFMs are to weak to capture the semantics of PDL with
intersection.}
}
@inproceedings{DKR-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
title = {Symbolic Bisimulation for the Applied Pi-Calculus},
pages = {133-145},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fsttcs07.pdf},
doi = {10.1007/978-3-540-77050-3_11},
abstract = {We propose a symbolic semantics for the finite applied pi
calculus, which is a variant of the pi calculus with extensions for
modelling cryptgraphic protocols. By~treating inputs symbolically, our
semantics avoids potentially infinite branching of execution trees due to
inputs from the environment. Correctness is maintained by associating with
each process a set of constraints on symbolic terms. Based on the
semantics, we~define a sound symbolic labelled bisimulation relation.
This~is an important step towards automation of observational equivalence
for the finite applied pi calculus, \emph{e.g.}, for verification of
anonymity or strong secrecy properties of protocols with a bounded number
of sessions.}
}
@inproceedings{DR-lpar07,
address = {Yerevan, Armenia},
month = oct,
year = 2007,
volume = 4790,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Dershowitz, Nachum and Voronkov, Andrei},
acronym = {{LPAR}'07},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'07)},
author = {Demri, St{\'e}phane and Rabinovich, Alexander},
title = {The complexity of temporal logic with until and since over ordinals},
pages = {531-545},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DR-lpar07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DR-lpar07.pdf},
doi = {10.1007/978-3-540-75560-9_38},
abstract = {We consider the temporal logic with since and until
modalities. This temporal logic is expressively equivalent over the
class of ordinals to first-order logic thanks to Kamp's theorem.
We~show that it has a PSPACE-complete satisfiability problem over the
class of ordinals. Among the consequences of our proof, we show that
given the code of some countable ordinal~\(\alpha\) and a formula, we
can decide in PSPACE whether the formula has a model over~\(\alpha\).
In~order to show these results, we~introduce a class of simple ordinal
automata, as expressive as B{\"u}chi ordinal automata. The PSPACE
upper bound for the satisfiability problem of the temporal logic is
obtained through a reduction to the nonemptiness problem for the
simple ordinal automata.}
}
@inproceedings{DLL-lpar07,
address = {Yerevan, Armenia},
month = oct,
year = 2007,
volume = 4790,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Dershowitz, Nachum and Voronkov, Andrei},
acronym = {{LPAR}'07},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'07)},
author = {Delaune, St{\'e}phanie and Lin, Hai and Lynch, {\relax Ch}ristopher},
title = {Protocol verification via rigid{\slash}flexible resolution},
pages = {242-256},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLL-lpar07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLL-lpar07.pdf},
doi = {10.1007/978-3-540-75560-9_19},
abstract = {In this paper we propose a decision procedure,
i.e., an~inference system for clauses containing rigid and
flexible variables. Rigid variables are only allowed to have
one instantiation, whereas flexible variables are allowed as
many instantiations as desired. We~assume a set of clauses
containing only rigid variables together with a set of clauses
containing only flexible variables. When the flexible clauses
fall into a particular class, we propose an inference system
based on ordered resolution that is sound and complete and for
which the inference procedure will halt.\par
An interest in this form of problem is for cryptographic
protocol verification for a bounded number of protocol
instances. Our class allows us to obtain a generic decidability
result for a large class of cryptographic protocols that may
use for instance~CBC (Cipher Block Chaining) encryption and
blind signature. }
}
@inproceedings{CD-lpar07,
address = {Yerevan, Armenia},
month = oct,
year = 2007,
volume = 4790,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Dershowitz, Nachum and Voronkov, Andrei},
acronym = {{LPAR}'07},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'07)},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Deciding Knowledge in Security Protocols for
Monoidal Equational Theories},
pages = {196-210},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-lpar07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-lpar07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CD-lpar07.ps},
doi = {10.1007/978-3-540-75560-9_16},
abstract = {In formal approaches, messages sent over a
network are usually modeled by terms together with an
equational theory, axiomatizing the properties of the
cryptographic functions (encryption, exclusive or,~...).
The~analysis of cryptographic protocols requires a
precise understanding of the attacker knowledge. Two
standard notions are usually used: deducibility and
indistinguishability. Only few results have been obtained
(in~an ad-hoc~way) for equational theories with
associative and commutative properties, especially in the
case of static equivalence. The~main contribution of this
paper is to propose a general setting for solving
deducibility and indistinguishability for an important
class (called monoidal) of these theories. Our~setting
relies on the correspondence between a monoidal
theory~{\(E\)} and a semiring~{\(S_E\)} which allows us
to give an algebraic characterization of the deducibility
and indistinguishability problems. As~a consequence we
recover easily existing decidability results and obtain
several new ones.}
}
@proceedings{secret2007-pre,
title = {{P}reliminary {P}roceedings of the 2nd
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'07)},
booktitle = {{P}reliminary {P}roceedings of the 2nd
{I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
({SecReT}'07)},
editor = {Nesi, Monica and Treinen, Ralf},
year = 2007,
month = jul,
address = {Paris, France}
}
@inproceedings{phs-time07,
address = {Alicante, Spain},
month = jun,
year = 2007,
publisher = {{IEEE} Computer Society Press},
editor = {Goranko, Valentin and Wang, X. Sean},
acronym = {{TIME}'07},
booktitle = {{P}roceedings of the 14th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'07)},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Model Checking Branching-Time Logics},
pages = {5},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phs-time07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phs-time07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-time07.ps},
doi = {10.1109/TIME.2007.52}
}
@inproceedings{CDP-formats07,
address = {Salzburg, Austria},
month = oct,
year = 2007,
volume = 4763,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Raskin, Jean-Fran{\c{c}}ois and Thiagarajan, P. S.},
acronym = {{FORMATS}'07},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'07)},
author = {Chevalier, Fabrice and D'Souza, Deepak and Prabhakar,
Pavithra},
title = {Counter-free Input Determined Timed Automata},
pages = {82-97},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-formats07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-formats07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDP-formats07.ps},
doi = {10.1007/978-3-540-75454-1_8},
abstract = {We identify a class of timed automata, which we call
counter-free input-determined automata, which characterize
the class of timed languages definable by several timed
temporal logics in the literature, including~MTL. We~make
use of this characterization to show that MTL+Past satisfies
an {"}ultimate stability{"} property with respect to periodic
sequences of timed words. Our results hold for both the
pointwise and continuous semantics. Along the way we
generalize the result of McNaughton-Papert to show a
counter-free automata characterization of FO-definable
finitely varying functions.}
}
@inproceedings{BM-formats07,
address = {Salzburg, Austria},
month = oct,
year = 2007,
volume = 4763,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Raskin, Jean-Fran{\c{c}}ois and Thiagarajan, P. S.},
acronym = {{FORMATS}'07},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'07)},
author = {Bouyer, Patricia and Markey, Nicolas},
title = {Costs are Expensive!},
pages = {53-68},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-formats07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-formats07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BM-formats07.ps},
doi = {10.1007/978-3-540-75454-1_6},
abstract = {We study the model-checking problem for WMTL,
a~cost-extension of the linear-time timed temporal logic MTL, that is
interpreted over weighted timed automata. We~draw a complete picture of
the decidability for that problem: it~is decidable only for the class of
one-clock weighted timed automata with a restricted stopwatch cost, and
any slight extension of this model leads to undecidability. We~finally
give some consequences on the undecidability of linear hybrid automata.}
}
@inproceedings{BCD-jouannaud,
address = {Cachan, France},
month = jun,
year = 2007,
volume = 4600,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
acronym = {{R}ewriting, {C}omputation and {P}roof},
booktitle = {{R}ewriting, {C}omputation and {P}roof~--- {E}ssays {D}edicated to
{J}ean-{P}ierre {J}ouannaud on the {O}ccasion of his 60th {B}irthday},
editor = {Comon{-}Lundh, Hubert and Kirchner, Claude and Kirchner,
H{\'e}l{\`e}ne},
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune,
St{\'e}phanie},
title = {Deducibility Constraints, Equational Theory and Electronic Money},
pages = {196-212},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-jpj07.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-jpj07.ps},
doi = {10.1007/978-3-540-73147-4_10},
abstract = {The starting point of this work is a case study (from France
T\'el\'ecom) of an electronic purse protocol. The~goal was to prove that
the protocol is secure or that there is an attack. Modeling the protocol
requires algebraic properties of a fragment of arithmetic, typically
containing modular exponentiation. The~usual equational theories described
in papers on security protocols are too weak: the~protocol cannot even be
executed in these models. We~consider here an equational theory which is
powerful enough for the protocol to be executed, and for which unification
is still decidable.\par
Our main result is the decidability of the so-called intruder deduction
problem, i.e.,~security in presence of a passive attacker, taking the
algebraic properties into account. Our~equational theory is a combination
of several equational theories over non-disjoint signatures.}
}
@proceedings{CLKK-jouannaud07,
editor = {Comon{-}Lundh, Hubert and Kirchner, Claude and Kirchner,
H{\'e}l{\`e}ne},
booktitle = {Rewriting, Computation and Proof~--- Essays Dedicated to
Jean-Pierre Jouannaud on the Occasion of his 60th Birthday},
title = {Rewriting, Computation and Proof~--- Essays Dedicated to
Jean-Pierre Jouannaud on the Occasion of his 60th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4600,
year = 2007,
month = jun,
address = {Cachan, France},
url = {http://www.springerlink.com/content/p0p40764x486/},
doi = {10.1007/978-3-540-73147-4},
isbn = {978-3-540-73146-7}
}
@phdthesis{chevalier-these2007,
author = {Chevalier, Fabrice},
title = {Logiques pour les syst{\`e}mes temporis{\'e}s~: contr{\^o}le et expressivit{\'e}},
year = 2007,
month = jun,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-FC07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-FC07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-FC07.ps}
}
@phdthesis{reynier-these2007,
author = {Reynier, Pierre-Alain},
title = {V{\'e}rification de syst{\`e}mes temporis{\'e}s et
distribu{\'e}s~: mod{\`e}les, algorithmes et impl{\'e}mentabilit{\'e}},
year = 2007,
month = jun,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-reynier.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-reynier.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-reynier.ps}
}
@phdthesis{demri-hab2007,
author = {Demri, St{\'e}phane},
title = {Logiques pour la sp{\'e}cification et v{\'e}rification},
year = 2007,
month = jun,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~7, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-habil07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-habil07.pdf},
futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
SD-habil-slides.ps.gz}
}
@phdthesis{encrenaz-hab2007,
author = {Encrenaz{-}Tiph{\`e}ne, Emmanuelle},
title = {Contributions pour la conception et la v{\'e}rification de
syst{\`e}mes mat{\'e}riels embarqu{\'e}s},
year = 2007,
month = jun,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~6, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EE-habil07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EE-habil07.pdf},
futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
EE-habil-slides.ps.gz}
}
@techreport{LSV:07:21,
author = {Chamseddine, Najla and Duflot, Marie and Fribourg, Laurent and Picaronny, Claudine},
title = {Determinate Probabilistic Timed Automata as {M}arkov Chains with
Parametric Costs},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = may,
type = {Research Report},
number = {LSV-07-21},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-21.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-21.pdf},
note = {17~pages},
abstract = {We consider probabilistic systems modeled under the form of a
special class of probabilistic timed automata. Such automata have {"}no
choice{"}: when the automaton arrives at a node, the time at which it will
leave it is determined; and when the automaton leaves the node, there is
just one distribution of target nodes.\par
In the paper, we give a method for computing the expected time~\(A\) for
the automaton to reach an {"}absorbing{"} node. Roughly speaking, the
method consists in putting the automaton under the form of a Markov chain
with costs (corresponding to durations). Under certain conditions, the
method is parametric in the sense that \(A\)~is computed as a function of
the constants appearing in the outgoing conditions and the invariants of
nodes, but does not assume known their explicit values.\par
We illustrate the method on the CSMA/CD protocol.}
}
@techreport{LSV:07:20,
author = {Bresciani, Riccardo},
title = {The {ZRTP} Protocol~--- Security Considerations},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = may,
type = {Research Report},
number = {LSV-07-20},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-20.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-20.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2007-20.ps},
note = {23~pages},
abstract = {ZRTP is draft of key agreement protocol by Phil~Zimmermann,
which relies on a Diffie-Hellman exchange to generate SRTP session
parameters, providing confidentiality and protecting against
\emph{Man-in-the-Middle} attacks even without a public key infrastructure or
endpoint certificates. This is an analysis of the protocol performed with
AVISPA and ProVerif, which tests security properties of ZRTP; in~order to
perform the analysis, the protocol has been modeled in HLPSL (for~AVISPA)
and in the applied \(\pi\)-calculus (for~Proverif). An improvement to gather
some extra resistance against \emph{Man-in-the-Middle} attacks is also proposed.}
}
@inproceedings{AMN-concur07,
address = {Lisbon, Portugal},
month = sep,
year = 2007,
volume = 4703,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
acronym = {{CONCUR}'07},
booktitle = {{P}roceedings of the 18th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'07)},
author = {Akshay, S. and Mukund, Madhavan and Narayan Kumar, K.},
title = {Checking Coverage for Infinite Collections of Timed Scenarios},
pages = {181-196},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AMN-concur07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AMN-concur07.pdf},
doi = { 10.1007/978-3-540-74407-8_13},
abstract = {We consider message sequence charts enriched with timing
constraints between pairs of events. As in the untimed setting, an
infinite family of time-constrained message sequence charts~(TC-MSCs) is
generated using an HMSC ---a finite-state automaton whose nodes are
labelled by TC-MSCs. A~timed MSC is an MSC in which each event is assigned
an explicit time-stamp. A~timed MSC covers a TC-MSC if it satisfies all
the time constraints of the~TC-MSC. A~natural recognizer for timed MSCs is
a message-passing automaton~(MPA) augmented with clocks. The~question we
address is the following: given a timed system specified as a
time-constrained HMSC H and an implementation in the form of a timed
MPA~\(A\), is~every TC-MSC generated by~\(H\) covered by some timed MSC
recognized by~\(A\)? We~give a complete solution for locally synchronized
time-constrained HMSCs, whose underlying behaviour is always regular.
We~also describe a restricted solution for the general case.}
}
@inproceedings{ACD-frocos07,
address = {Liverpool, UK},
month = sep,
year = 2007,
volume = 4720,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Wolter, Franck},
acronym = {{FroCoS}'07},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {F}rontiers of
{C}ombining {S}ystems ({FroCoS}'07)},
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune,
St{\'e}phanie},
title = {Combining algorithms for deciding knowledge in security
protocols},
pages = {103-117},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-frocos07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-frocos07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACD-frocos07.ps},
doi = {10.1007/978-3-540-74621-8_7},
abstract = {In formal approaches, messages sent over a network are
usually modeled by terms together with an equational theory,
axiomatizing the properties of the cryptographic functions
(encryption, exclusive or,~...). The analysis of
cryptographic protocols requires a precise understanding of
the attacker knowledge. Two standard notions are usually
used: deducibility and indistinguishability. Those notions
are well-studied and a lot of decidability results already
exist to deal with a variety of equational theories.\par
We~show that decidability results can be easily combined for
any disjoint equational theories: if the deducibility and
indistinguishability relations are decidable for two
disjoint theories, they are also decidable for their union.
As~an application, new decidability results can be obtained
using this combination theorem.}
}
@inproceedings{KM-esorics07,
address = {Dresden, Germany},
month = sep,
year = 2007,
volume = 4734,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Biskup, Joachim and Lopez, Javier},
acronym = {{ESORICS}'07},
booktitle = {{P}roceedings of the 12th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'07)},
author = {Kremer, Steve and Mazar{\'e}, Laurent},
title = {Adaptive Soundness of Static Equivalence},
pages = {610-625},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-esorics07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-esorics07.pdf},
doi = {10.1007/978-3-540-74835-9_40},
abstract = {We define a framework to reason about implementations of
equational theories in the presence of an adaptive adversary. We
particularly focus on soundess of static equivalence. We illustrate our
framework on several equational theories: symmetric encryption, XOR,
modular exponentiation and also joint theories of encryption and modular
exponentiation. This last example relies on a combination result for
reusing proofs for the separate theories. Finally, we~define a model for
symbolic analysis of dynamic group key exchange protocols, and show its
computational soundness.}
}
@inproceedings{BLMO-concur07,
address = {Lisbon, Portugal},
month = sep,
year = 2007,
volume = 4703,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
acronym = {{CONCUR}'07},
booktitle = {{P}roceedings of the 18th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'07)},
author = {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas and Oreiby, Ghassan},
title = {Timed Concurrent Game Structures},
pages = {445-459},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMO-concur07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMO-concur07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLMO-concur07.ps},
doi = {10.1007/978-3-540-74407-8_30},
abstract = {We propose a new model for timed games, based on concurrent game
structures~(CGSs). Compared to the classical \emph{timed game automata}
of~Asarin \emph{et~al.}, our timed~CGSs are {"}more concurrent{"}, in the
sense that they always allow all the agents to act on the system,
independently of the delay they want to elapse before their action. Timed
CGSs weaken the {"}element of surprise{"} of timed game automata reported
by de~Alfaro \emph{et~al.}\par
We prove that our model has nice properties, in particular that
model-checking timed CGSs against timed \(\textsf{ATL}\) is decidable
\emph{via} region abstraction, and in particular that strategies are
{"}region-stable{"} if winning objectives are. We also propose a new
extension of \(\textsf{TATL}\), containing~\(\textsf{ATL}^{*}\), which we
call~\(\textsf{TALTL}\). We~prove that model-checking this logic remains
decidable on timed CGSs. Last, we explain how our algorithms can be
adapted in order to rule out Zeno (co-)strategies, based on the ideas of
Henzinger \emph{et~al.}}
}
@inproceedings{Gou-csl07,
address = {Lausanne, Switzerland},
month = sep,
year = 2007,
volume = 4646,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Duparc, Jacques and Henzinger, {\relax Th}omas A.},
acronym = {{CSL}'07},
booktitle = {{P}roceedings of the 16th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'07)},
author = {Goubault{-}Larrecq, Jean},
title = {Continuous Previsions},
pages = {542-557},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf},
doi = {10.1007/978-3-540-74915-8_40},
abstract = {We define strong monads of continuous (lower, upper) previsions,
and of forks, modeling both probabilistic and non-deterministic choice.
This is an elegant alternative to recent proposals by Mislove, Tix,
Keimel, and Plotkin. We show that our monads are sound and complete, in
the sense that they model exactly the interaction between probabilistic
and (demonic, angelic, chaotic) choice.}
}
@article{bozzelli-tcs07,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bozzelli, Laura},
title = {Complexity results on branching-time pushdown model checking},
year = 2007,
volume = 379,
number = {1-2},
pages = {286-297},
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bozzelli-tcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bozzelli-tcs07.pdf},
doi = {10.1016/j.tcs.2007.03.049},
abstract = {The model checking problem of pushdown systems (PMC~problem,
for~short) against standard branching temporal logics has been intensively
studied in the literature. In particular, for the modal \(\mu\)-calculus,
the most powerful branching temporal logic used for verification, the
problem is known to be EXPTIME-complete (even~for a fixed~formula).
The~problem remains EXPTIME-complete also for the logic~CTL, which
corresponds to a fragment of the alternation-free modal \(\mu\)-calculus.
For~the logic~CTL\(^{*}\), the problem is known to be in 2EXPTIME. In~this
paper, we~show that the complexity of the PMC problem for CTL\(^{\*}\) is
in fact 2EXPTIME-complete. Moreover, we give a new optimal algorithm to
solve this problem based on automata theoretic techniques. Finally, we
prove that the program complexity of the PMC problem against CTL
(i.e.,~the complexity of the problem in terms of the size of the~system)
is EXPTIME-complete.}
}
@inproceedings{BGMN-fct07,
address = {Budapest, Hungary},
month = aug,
year = 2007,
volume = 4639,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and {\'E}sik, Zolt{\'a}n},
acronym = {{FCT}'07},
booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium
on {F}undamentals of {C}omputation {T}heory
({FCT}'07)},
author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan and Narayan
Kumar, K.},
title = {Local testing of message sequence charts is difficult},
pages = {76-87},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
doi = {10.1007/978-3-540-74240-1_8},
abstract = {Message sequence charts are an attractive visual formalism used
to specify distributed communicating systems. One~way to test such a
system is to substitute a component by a test process and observe its
interaction with the rest of the system. We~study the question of whether
we can characterize the distributed behaviour of the system based on such
local observations. The~main difficulty is that local observations can
combine in unexpected ways to define implied scenarios not present in the
original specification. It~is known that checking whether a scenario
specification is closed with respect to implied scenarios is undecidable
when observations are made one process at a time, even for regular
specifications. We~show that this undecidability holds even if we have
only two processes in the system. We then strengthen the observer to be
able to observe multiple processes simultaneously. Even in this stronger
framework, the problem remains undecidable. In~fact, undecidability
continues to hold even without message labels, provided we observe two or
more processes simultaneously. On~the other hand, if we do not have
message labels and we restrict observations to one process at a time, the
problem of checking for implied scenarios is decidable.}
}
@inproceedings{GM-spin07,
address = {Berlin, Germany},
month = jul,
year = 2007,
volume = 4595,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bo{\v{s}}nacki, Dragan and Edelkamp, Stefan},
acronym = {{SPIN}'07},
booktitle = {{P}roceedings of the 14th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'07)},
author = {Gastin, Paul and Moro, Pierre},
title = {Minimal counter-example generation for {SPIN}},
pages = {24-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-spin07.ps},
doi = {10.1007/978-3-540-73370-6_4},
abstract = {In this paper, we propose an algorithm to compute a counter-example of
minimal size to some property in a finite state program, using the same
programmation constraints than~SPIN. This algorithm uses nested
Breadth-first searches guided by priority queues.
This algorithm works in quadratic time and is linear in memory.}
}
@article{GK-fi07,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Uniform satisfiability in {PSPACE} for local temporal logics
over {M}azurkiewicz traces},
volume = 80,
number = {1-3},
pages = {169-197},
year = 2007,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
abstract = {We study the complexity of temporal logics over
concurrent systems that can be described by Mazurkiewicz traces. We
develop a general method to prove that the uniform satisfiability
problem of local temporal logics is in~PSPACE. We~also
demonstrate that this method applies to all known local temporal
logics.}
}
@techreport{DGA:rap3,
author = {Lafourcade, Pascal},
title = {Rapport final d'activit{\'e} {\`a}~{\(11\)}~mois, contrat~{CNRS/DGA}
r{\'e}f{\'e}rence~: 06~60~019~00~470~75~01
<<~{U}tilisation et exploitation des th{\'e}ories {\'e}quationnelles
dans l'analyse des protocoles cryptographiques~>>},
type = {Contract Report},
institution = {DGA},
year = {2007},
month = oct,
note = {6~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap3.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap3.ps}
}
@techreport{DGA:rap2,
author = {Lafourcade, Pascal},
title = {Rapport d'activit{\'e}s {\`a}~{\(6\)}~mois, contrat~{CNRS/DGA}
r{\'e}f{\'e}rence~: 06~60~019~00~470~75~01
<<~{U}tilisation et exploitation des th{\'e}ories {\'e}quationnelles
dans l'analyse des protocoles cryptographiques~>>},
type = {Contract Report},
institution = {DGA},
year = {2007},
month = apr,
note = {5~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap2.ps}
}
@techreport{DGA:rap1,
author = {Lafourcade, Pascal},
title = {Rapport d'activit{\'e}s {\`a}~{\(3\)}~mois, contrat~{CNRS/DGA}
r{\'e}f{\'e}rence~: 06~60~019~00~470~75~01
<<~{U}tilisation et exploitation des th{\'e}ories {\'e}quationnelles
dans l'analyse des protocoles cryptographiques~>>},
type = {Contract Report},
institution = {DGA},
year = {2007},
month = jan,
note = {3~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap1.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap1.ps}
}
@inproceedings{DG-time07,
address = {Alicante, Spain},
month = jun,
year = 2007,
publisher = {{IEEE} Computer Society Press},
editor = {Goranko, Valentin and Wang, X. Sean},
acronym = {{TIME}'07},
booktitle = {{P}roceedings of the 14th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'07)},
author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
title = {The Effects of Bounding Syntactic Resources on {P}resburger
{LTL} (Extended Abstract)},
pages = {94-104},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-time07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-time07.pdf},
doi = {10.1109/TIME.2007.63},
abstract = {We study decidability and complexity issues for fragments of LTL
with Presburger constraints by restricting the syntactic resources of the
formulae (the~class of constraints, the number of variables and the
distance between two states for which counters can be compared) while
preserving the strength of the logical operators. We provide a complete
picture refining known results from the literature, in some cases pushing
forward the known decidability limits. By~way of example, we show that
model-checking formulae from LTL with quantifier-free Presburger
arithmetic over one-counter automata is only PSPACE-complete. In~order to
establish the PSPACE upper bound, we show that the nonemptiness problem
for Buchi one-counter automata taking values in~\(\mathbb{Z}\) and
allowing zero tests and sign tests, is only NLOGSPACE-complete.}
}
@article{BGP-fmsd07,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit,
Antoine},
title = {Timed substitutions for regular signal-event languages},
volume = 31,
number = 2,
pages = {101-134},
year = 2007,
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
doi = {10.1007/s10703-007-0034-5},
abstract = {In the classical framework of formal languages, a refinement
operation is modeled by a substitution and an abstraction by an inverse
substitution. These mechanisms have been widely studied, because they
describe a change in the specification level, from an abstract view to a
more concrete one, or conversely. For timed systems, there is up to now no
uniform notion of substitution. In~this paper, we~study timed substitutions
in the general framework of signal-event languages, where both signals and
events are taken into account. We prove that regular signal-event languages
are closed under substitution and inverse substitution.\par
To obtain these results, we use in a crucial way a {"}well known{"} result:
regular signal-event languages are closed under intersection. In fact,
while this result is indeed easy for languages defined by Alur and Dill's
timed automata, it turns out that the construction is much more tricky when
considering the most involved model of signal-event automata. We give here
a construction working on finite and infinite signal-event words and taking
into account signal stuttering, unobservability of zero-duration \(\tau\)-signals
and Zeno runs. Note that if several constructions have been proposed in
particular cases, it is the first time that a general construction is
provided.}
}
@inproceedings{JGL-icalp07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
volume = 4596,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arge, Lars and Cachin, {\relax Ch}ristian and Jurdzi{\'n}ski, Tomasz
and Tarlecki, Andrzej},
acronym = {{ICALP}'07},
booktitle = {{P}roceedings of the 34th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'07)},
author = {Goubault{-}Larrecq, Jean},
title = {Continuous Capacities on Continuous State Spaces},
pages = {764-776},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf},
doi = {10.1007/978-3-540-73420-8_66},
abstract = {We propose axiomatizing some stochastic games, in a
continuous state
space setting, using continuous belief functions, resp.
plausibilities, instead of measures. Then, stochastic games are
just variations on continuous Markov chains. We argue that drawing
at random along a belief function is the same as letting the
probabilistic player~\(P\) play first, then letting the
non-deterministic player~\(C\) play demonically. The same
holds for an angelic~\(C\), using plausibilities instead.
We then define a simple modal logic, and characterize simulation in
terms of formulae of this logic. Finally, we show that (discounted)
payoffs are defined and unique, where in the demonic case,
\(P\)~maximizes payoff, while \(C\)~minimizes it}
}
@inproceedings{BHPR-icalp07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
volume = 4596,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arge, Lars and Cachin, {\relax Ch}ristian and Jurdzi{\'n}ski, Tomasz
and Tarlecki, Andrzej},
acronym = {{ICALP}'07},
booktitle = {{P}roceedings of the 34th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'07)},
author = {Brihaye, {\relax Th}omas and Henzinger, {\relax Th}omas A. and
Prabhu, Vinayak and Raskin, Jean-Fran{\c{c}}ois},
title = {Minimum-Time Reachability in Timed Games},
pages = {825-837},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHPR-icalp07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHPR-icalp07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHPR-icalp07.ps},
doi = {10.1007/978-3-540-73420-8_71},
abstract = {We consider the minimum-time reachability problem in concurrent
two-player timed automaton game structures. We~show how to compute the
minimum time needed by a player to reach a location against all possible
choices of the opponent. We~do not put any syntactic restriction on the
game structure, nor do we require any player to guarantee time divergence.
We~only require players to use physically realizable strategies.
The~minimal time is computed in part using a fixpoint expression which we
show can be used on equivalence classes of a non-trivial extension of the
region equivalence relation.}
}
@inproceedings{CDS-csf07,
address = {Venice, Italy},
month = jul,
year = 2007,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'07},
booktitle = {{P}roceedings of the
20th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'07)},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and Steel, Graham},
title = {A Formal Theory of Key Conjuring},
pages = {79-93},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDS-csf07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDS-csf07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDS-csf07.ps},
doi = {10.1109/CSF.2007.5},
abstract = {We describe a formalism for \emph{key conjuring}, the process by
which an attacker obtains an unknown, encrypted key by repeatedly calling
a cryptographic API function with random values in place of keys. This
technique has been used to attack the security APIs of several Hardware
Security Modules~(HSMs), which are widely deployed in the ATM (cash
machine) network. We~propose a formalism for detecting computationally
feasible key conjuring operations, incorporated into a Dolev-Yao style
model of the security~API. We~show that security in the presence of key
conjuring operations is decidable for a particular class of~APIs, which
includes the key management~API of IBM's Common Cryptographic
Architecture~(CCA).}
}
@inproceedings{Gou-lics07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'07},
booktitle = {{P}roceedings of the 22nd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'07)},
author = {Goubault{-}Larrecq, Jean},
title = {On {N}oetherian Spaces},
pages = {453-462},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf},
doi = {10.1109/LICS.2007.34},
abstract = {A topological space is Noetherian iff every open is compact.
Our~starting point is that this notion generalizes that of
well-quasi order, in the sense that an Alexandroff-discrete space is
Noetherian iff its specialization quasi-ordering is well. For~more
general spaces, this opens the way to verifying infinite transition
systems based on non-well quasi ordered sets, but where the preimage
operator satisfies an additional continuity assumption. The
technical development rests heavily on techniques arising from
topology and domain theory, including sobriety and the de Groot dual
of a stably compact space. We~show that the category Nthr of
Noetherian spaces is finitely complete and finitely cocomplete.
Finally, we note that if \(X\)~is a Noetherian space, then the set of
all (even infinite) subsets of~\(X\) is again Noetherian, a~result
that fails for well-quasi orders.}
}
@inproceedings{BMOW-lics07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'07},
booktitle = {{P}roceedings of the 22nd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'07)},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and
Worrell, James},
title = {The Cost of Punctuality},
pages = {109-118},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-lics07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-lics07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMOW-lics07.ps},
doi = {10.1109/LICS.2007.49},
abstract = {In an influential paper titled {"}The Benefits of
Relaxing Punctuality{"}, Alur, Feder, and~Henzinger introduced
Metric Interval Temporal Logic~(MITL) as a fragment of the real-time
logic Metric Temporal Logic~(MTL) in which exact or punctual timing
constraints are banned. Their main result showed that model checking and
satisfiability for~MITL are both EXPSPACE-Complete.\par
Until recently, it was widely believed that admitting even the simplest
punctual specifications in any linear-time temporal logic would
automatically lead to undecidability. Although this was recently
disproved, until now no punctual fragment of~MTL was known to have even
primitive recursive complexity (with certain decidable fragments having
provably non-primitive recursive complexity).\par
In this paper we identify a `co-flat' subset of~MTL that is capable of
expressing a large class of punctual specifications and for which model
checking (although not satisfiability) has no complexity cost over~MITL.
Our logic is moreover qualitatively different from~MITL in that it can
express properties that are not timed-regular. Correspondingly, our
decision procedures do not involve translating formulas into
finite-state automata, but rather into certain kinds of reversal-bounded
Turing machines. Using this translation we show that the model checking
problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete
if timing constraints are encoded in unary.}
}
@inproceedings{BDL-hav07,
address = {Braga, Portugal},
month = mar,
year = 2007,
editor = {Berdine, Josh and Sagiv, Mooly},
acronym = {{HAV}'07},
booktitle = {{P}roceedings of the 1st {W}orkshop on {H}eap {A}nalysis and
{V}erification ({HAV}'07)},
author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
title = {Reasoning about Sequences of Memory States},
preliminary-version-of = {BDL-lfcs2007},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-hav07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-hav07.pdf},
abstract = {In order to verify programs with pointer variables,
we introduce a temporal logic LTL\textsuperscript{mem} whose
underlying
assertion language is the
quantifier-free fragment of separation logic and the temporal logic on
the
top of it is the standard linear-time temporal logic~LTL. We~state
the
complexity of various model-checking and satisfiability problems for
LTL\textsuperscript{mem} , considering various
fragments of separation logic (including pointer arithmetic), various
classes of models (with or without constant heap), and the influence
of fixing the initial memory state.
Our main decidability result is PSPACE-completeness of the
satisfiability problems on the record fragment and on a classical
fragment allowing pointer arithmetic.
\(\Sigma^{0}_{1}\)-completeness or \(\Sigma^{1}_{1}\)-completeness
results
are established for various problems, and underline the tightness of
our decidability results.}
}
@techreport{LSV:07:10,
author = {Bouhoula, Adel and Jacquemard, Florent},
title = {Tree Automata, Implicit Induction and Explicit Destructors for
Security Protocol Verification},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = feb,
type = {Research Report},
number = {LSV-07-10},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-10.pdf},
note = {21~pages},
abstract = {We present a new method for automatic implicit induction theorem
proving, and its application for the verification of cryptographic
protocols. The~method is based on constrained tree grammars and handles
non-confluent rewrite systems which are required in the context of the
verification of security protocols because of the non-deterministic
behavior of attackers. It~also handles axioms between constructor terms
which allows us to specify explicit destructors representing cryptographic
operators. Constrained tree grammars are used in our procedure both as
induction schemes and as oracles for checking validity and redundancy by
reduction to an emptiness problem. They also permit to characterize
security failure of cryptographic protocols as sets of execution traces
corresponding to an attack. This~way, we obtain a generic framework for
the verification of protocols, in~which we can verify reachability
properties like confidentiality, but also more complex properties like
authentication. We present three case studies which gave very promising
results.}
}
@techreport{KL-eth07,
author = {Ksi{\k e}{\. z}opolski, Bogdan and Lafourcade, Pascal},
title = {Attack and Revison of an Electronic Auction Protocol using~{OFMC}},
institution = {Department of Computer Science, ETH Zurich, Switzerland},
year = 2007,
month = feb,
type = {Technical Report},
number = {549},
note = {13~pages},
nmnote = {on peut pas dire que ce soit un papier du labo... Si en fait,
car Pascal etait la-bas sur un contrat gere par le LSV},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KL-eth549.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KL-eth549.pdf},
abstract = {In the article we show an attack on the cryptographic protocol
of electronic auction with extended requirements
[Ksiezopolski and Kotulski, \textit{Cryptographic protocol
for electronic auctions with extended requirements},~2004].
The found attack consists of authentication breach and
secret retrieval. It~is a kind of {"}man-in-the-middle
attack{"}. The intruder impersonates an agent and learns some
secret information. We have discovered this flaw unsing OFMC
an automatic tool of cryptographic protocol verification.
After a description of this attack, we propose a new version
of the e-auction protocol. We also check with OFMC the
secrecy for the new protocol and give an informal proof of
the other properties that this new e-auction protocol has to
guarantee.}
}
@inproceedings{Maz-wits07,
address = {Braga, Portugal},
month = mar,
year = 2007,
editor = {Focardi, Riccardo},
acronym = {{WITS}'07},
booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational {W}orkshop
on {I}ssues in the {T}heory of {S}ecurity ({WITS}'07)},
author = {Mazar{\'e}, Laurent},
title = {Computationally Sound Analysis of Protocols using Bilinear Pairings},
pages = {6-21},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Maz-wits07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Maz-wits07.pdf},
abstract = {In this paper, we introduce a symbolic model to analyse
protocols that use a bilinear pairing between two cyclic groups. This
model consists in an extension of the Abadi-Rogaway logic and we prove
that the logic is still computationally sound: symbolic
indistinguishability implies computational indistinguishability provided
that the Bilinear Decisional Diffie-Hellman assumption is verified and
that the encryption scheme is IND-CPA secure. We~illustrate our results on
classical protocols using bilinear pairing like Joux tripartite
Diffie-Hellman protocol or the TAK-2 and TAK-3 protocols.}
}
@inproceedings{BDL-lfcs2007,
address = {New~York, New~York, USA},
month = jun,
year = 2007,
volume = 4514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
acronym = {{LFCS}'07},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'07)},
author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
title = {Reasoning about sequences of memory states},
pages = {100-114},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-lfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-lfcs07.pdf},
doi = { 10.1007/978-3-540-72734-7_8},
abstract = {Motivated by the verification of programs with pointer
variables, we introduce a temporal logic LTL\textsuperscript{mem} whose
underlying assertion language is the quantifier-free fragment of
separation logic and the temporal logic on the top of it is the standard
linear-time temporal logic~LTL. We analyze the complexity of various
model-checking and satisfiability problems for LTL\textsuperscript{mem},
considering various fragments of separation logic (including pointer
arithmetic), various classes of models (with or without constant heap),
and the influence of fixing the initial memory state. We~provide a
complete picture based on these criteria. Our main decidability result is
PSPACE-completeness of the satisfiability problems on the record fragment
and on a classical fragment allowing pointer arithmetic.
\(\Sigma^{0}_{1}\)-completeness or \(\Sigma^{1}_{1}\)-completeness
results are established for various problems by reducing standard problems
for Minsky machines, and underline the tightness of our decidability
results.}
}
@inproceedings{BK-lata2007,
address = {Tarragona, Spain},
month = mar # {-} # apr,
year = 2007,
futureseries = {Lecture Notes in Computer Science},
nmnote = {published as Report 35/07 Research Group on Mathematical
Linguistics, Universitat Rovira i Virgili, Tarragona},
editor = {{\'E}sik, Zolt{\'a}n and Mart{\'\i}n-Vide, Carlos and
Mitrana, Victor},
acronym = {{LATA}'07},
booktitle = {{P}reliminary {P}roceedings of the 1st {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'07)},
author = {Bollig, Benedikt and Kuske, Dietrich},
title = {{M}uller Message-Passing Automata and Logics},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-lata07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-lata07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BK-lata07.ps},
abstract = {We study nonterminating message-passing automata whose behavior
is described by infinite message sequence charts. As~a~first result, we
show that Muller, B{\"u}chi, and termination-detecting Muller acceptance are
equivalent for these devices. To describe the expressive power of these
automata, we give a logical characterization. More precisely, we show that
they have the same expressive power as the existential fragment of a
monadic second-order logic featuring a first-order quantifier to express
that there are infinitely many elements satisfying some property. Our
result is based on a new extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e}
game to cope with infinite structures and the new first-order quantifier.}
}
@techreport{LSV:07:03,
author = {Goubault{-}Larrecq, Jean},
title = {Believe It Or Not, {GOI}~is a Model of Classical Linear Logic},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = jan,
type = {Research Report},
number = {LSV-07-03},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-03.pdf},
note = {18~pages},
othernote = {a draft of the longer version of this report is available at
http://www.lsv.ens-cachan.fr/~goubault/isg.pdf},
abstract = {We introduce the Danos-R\'egnier category \(\mathcal{DR}(M)\) of a linear
inverse monoid~\(M\), a categorical description of geometries of
interaction~(GOI). The usual setting for GOI is that of a weakly
Cantorian linear inverse monoid. It is well-known that GOI is
perfectly suited to describe the multiplicative fragment of linear
logic, and indeed \(\mathcal{DR}(M)\) will be a \(*\)-autonomous category in this
case. It is also well-known that the categorical interpretation of
the other linear connectives conflicts with GOI interpretations. We
make this precise, and show that \(\mathcal{DR}(M)\) has no terminal object, no
cartesian product, and no exponential---whatever \(M\) is, unless \(M\)
is trivial. However, a form of coherence completion of~\(\mathcal{DR}(M)\) \`a
la Hu-Joyal provides a model of full classical linear logic, as soon
as \(M\) is weakly Cantorian.}
}
@article{LS-ipl07,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Laroussinie, Fran{\c{c}}ois and Sproston, Jeremy},
title = {State Explosion in Almost-Sure Probabilistic Reachability},
year = 2007,
volume = {102},
number = {6},
pages = {236-241},
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LS-ipl07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LS-ipl07.pdf},
doi = {10.1016/j.ipl.2007.01.003},
abstract = {We show that the problem of reaching a state set with
probability~\(1\) in probabilistic-nondeterministic systems operating in
parallel is EXPTIME-complete. We then show that this probabilistic
reachability problem is EXPTIME-complete also for probabilistic timed
automata.}
}
@article{DO-fi2007,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
title = {Relative Nondeterministic Information Logic is
{EXPTIME}-complete},
year = {2007},
volume = {75},
number = {1-4},
pages = {163-178},
nmnote = {Special issue in memory of Z.~Paw{\l}ak},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DO-fi07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DO-fi07.pdf},
abstract = {We define a relative version of the logic NIL introduced by
Or{\l}owska, Paw{\l}ak and Vakarelov and we show that its
satisfiability is not only decidable but also
EXPTIME-complete. Such a logic combines two ingredients that
are seldom present simultaneously in information logics:
frame conditions involving more than one information
relation and relative frames. The~EXPTIME upper bound is
obtained by designing a well-suited decision procedure based
on the nonemptiness problem of B{\"u}chi automata on
infinite trees. The paper provides evidence that B{\"u}chi
automata on infinite trees are crucial language acceptors
even for relative information logics with multiple types of
relations.}
}
@techreport{LSV:07:02,
author = {Reynier, Pierre-Alain},
title = {Diagonal constraints handled efficiently in~{UPPAAL}},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = jan,
type = {Research Report},
number = {LSV-07-02},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-02.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2007-02.ps},
note = {4~pages},
abstract = {Timed automata (TA) are widely used to model real-time systems,
and UPPAAL is one of the most popular model-checker for this framework which
has been successfully applied over numerous industrial case studies. Diagonal
constraints are a natural extension of TA, that does not increase expressive
power, but gives conciseness. Unfortunately the classical forward algorithm
for reachability analysis cannot be used to deal directly with diagonal
constraints. Thus the current method implemented consists in removing them
on-the-fly, which implies a complexity blow-up. In~[P.~Bouyer, F.~Laroussinie,
and P.-A.~Reynier. \textit{Diagonal constraints in timed automata: Forward analysis of
timed systems}. Proceedings of FORMATS'06, LNCS~3829, p.~112-126, Springer], a
counter-example guided refinement algorithm has been proposed. In~this paper,
we present its implementation, and give some benchmarks on a variant of
Fischer's protocol. }
}
@phdthesis{THESE-baudet07,
author = {Baudet, Mathieu},
title = {S{\'e}curit{\'e} des protocoles cryptographiques~:
aspects logiques et calculatoires},
year = 2007,
month = jan,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baudet.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baudet.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-baudet.ps},
abstract = {This thesis is dedicated to the automatic verification of
cryptographic protocols in the logical and computational settings. \par
The~first part concerns the security of procotols in the logical
({"}formal{"}) framework. To~begin with, we show how to specify various
security properties of protocols in a concurrent language, and how to
analyze them automatically for a bounded number of sessions.
The~properties under consideration include notably simple secrecy,
authentication and resistance to dictionary attacks. \par
The~second part deals with the computational soundness of logical models.
The~main question here is to what extent the fact that no logical attack
exists on a protocol implies that it is provably secure in the usual
cryptographic model (called the computational model). We~concentrate on
static equivalence, applied notably to several kinds of encryption and
data vulnerable to dictionary attacks (such as passwords). We~show that
under simple conditions, any (logical) proof of static equivalence between
two messages implies their (computational) indistinguishability. This
entails computational soundness in the passive case for the notion of
dictionary attacks developped in the first part.}
}
@inproceedings{BM-lfcs2007,
address = {New~York, New~York, USA},
month = jun,
year = 2007,
volume = 4514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
acronym = {{LFCS}'07},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'07)},
author = {Bollig, Benedikt and Meinecke, Ingmar},
title = {Weighted Distributed Systems and Their Logics},
pages = {54-68},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-lfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-lfcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BM-lfcs07.ps},
doi = {10.1007/978-3-540-72734-7_5},
abstract = {We provide a model of weighted distributed systems and give a
logical characterization thereof. Distributed systems are represented as
weighted asynchronous cellular automata. Running over directed acyclic
graphs, Mazurkiewicz traces, or (lossy) message sequence charts, they
allow for modeling several communication paradigms in a unifying
framework, among them probabilistic shared-variable and probabilistic
lossy-channel systems. We~show that any such system can be described by a
weighted existential MSO formula and, vice versa, any formula gives rise
to a weighted asynchronous cellular automaton.}
}
@inproceedings{DDG-lfcs2007,
address = {New~York, New~York, USA},
month = jun,
year = 2007,
volume = 4514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
acronym = {{LFCS}'07},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'07)},
author = {Demri, St{\'e}phane and D'Souza, Deepak and Gascon, R{\'e}gis},
title = {Decidable Temporal Logic with Repeating Values},
pages = {180-194},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDG-lfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDG-lfcs07.pdf},
doi = {10.1007/978-3-540-72734-7_13},
abstract = {Various logical formalisms with the freeze quantifier have been
recently considered to model computer systems even though this is a
powerful mechanism that often leads to undecidability. In~this paper, we
study a linear-time temporal logic with past-time operators such that the
freeze operator is only used to express that some value from an infinite
set is repeated in the future or in the past. Such a restriction has been
inspired by a recent work on spatio-temporal logics. We~show decidability
of finitary and infinitary satisfiability by reduction into the
verification of temporal properties in Petri nets. This is a surprising
result since the logic is closed under negation, contains future-time and
past-time temporal operators and can express the nonce property and its
negation. These ingredients are known to lead to undecidability with a
more liberal use of the freeze quantifier. The~paper contains also
insights about the relationships between temporal logics with the freeze
operator and counter automata.}
}
@inproceedings{BBC-lfcs2007,
address = {New~York, New~York, USA},
month = jun,
year = 2007,
volume = 4514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
acronym = {{LFCS}'07},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'07)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Chevalier, Fabrice},
title = {Weighted O-Minimal Hybrid Systems are more
Decidable than Weighted Timed Automata!},
pages = {69-83},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lfcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lfcs07.ps},
doi = {10.1007/978-3-540-72734-7_6},
abstract = {We consider weighted o-minimal hybrid systems, which
extend classical o-minimal hybrid systems with cost functions. These cost
functions are {"}observer variables{"} which increase while the system evolves
but do not constrain the behaviour of the system. In this paper, we prove
two main results: (i)~optimal o-minimal hybrid games are decidable; (ii)~the
model-checking of~WCTL, an extension of CTL which can constrain the cost
variables, is decidable over that model. This has to be compared with the
same problems in the framework of timed automata where both problems are
undecidable in general, while they are decidable for the restricted class of
one-clock timed automata. }
}
@article{VG-icomp2007,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean},
title = {Alternating Two-Way {AC}-Tree Automata},
pages = {817-869},
year = {2007},
month = jun,
volume = 205,
number = 6,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VG-icomp07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VG-icomp07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VG-icomp07.ps},
doi = {10.1016/j.ic.2006.12.006},
abstract = {We explore the notion of alternating two-way tree automata
modulo the theory of finitely many associative-commutative
(AC) symbols. This was prompted by questions arising in
cryptographic protocol verification, in~particular in
modeling group key agreement schemes based on
Diffie-Hellman-like functions, where the emptiness question
for intersections of such automata is fundamental. This also
has independent interest. We~show that the use of general
push clauses, or of alternation, leads to undecidability,
already in the case of one AC symbol, with only functions of
arity zero. On~the other hand, emptiness is decidable in the
general case of several function symbols, including several
AC symbols, provided push clauses are unconditional and
intersection clauses are final. This class of automata is
also shown to be closed under intersection.}
}
@inproceedings{JLS-tacas07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = {4424},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Grumberg, Orna and Huth, Michael},
acronym = {{TACAS}'07},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'07)},
author = {Jurdzi{\'n}ski, Marcin and Laroussinie, Fran{\c{c}}ois and
Sproston, Jeremy},
title = {Model Checking Probabilistic Timed Automata with One or Two Clocks},
pages = {170-184},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JLS-tacas07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JLS-tacas07.pdf},
doi = {10.1007/978-3-540-71209-1_15},
abstract = {Probabilistic timed automata are an extension of timed automata
with discrete probability distributions. We~consider model-checking
algorithms for the subclasses of probabilistic timed automata which
have one or two clocks. Firstly, we show that PCTL probabilistic
model-checking problems (such~as determining whether a set of target
states can be reached with probability at least~0.99 re- gardless of
how nondeterminism is resolved) are PTIME-complete for one clock
probabilistic timed automata, and are EXPTIME-complete for
probabilistic timed automata with two clocks. Secondly, we show that
the model-checking problem for the probabilistic timed temporal logic
PTCTL is EXPTIME-complete for one clock probabilistic timed automata.
However, the corresponding model-checking problem for the subclass of
PTCTL which does not permit both (1)~punctual tim- ing bounds, which
require the occurrence of an event at an exact time point, and
(2)~comparisons with probability bounds other than 0 or~1, is
PTIME-complete.}
}
@inproceedings{DADSS-tacas07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = {4424},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Grumberg, Orna and Huth, Michael},
acronym = {{TACAS}'07},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'07)},
author = {D'Aprile, Davide and Donatelli, Susanna and Sangnier,
Arnaud and Sproston, Jeremy},
title = {From Time {P}etri Nets to Timed Automata: An Untimed
Approach},
pages = {216-230},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DADSS-tacas07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DADSS-tacas07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DADSS-tacas07.ps},
doi = {10.1007/978-3-540-71209-1_18},
abstract = {Time Petri Nets~(TPN) and Timed Automata~(TA) are widely-used
formalisms for the modeling and analysis of timed systems. A
recently-developed approach for the analysis of TPNs concerns
their translation to~TAs, at which point efficient analysis
tools for TAs can then be applied. One~feature of much of this
previous work has been the use of timed reachability analysis on
the TPN in order to construct the~TA. In this paper we present a
method for the translation from TPNs to~TAs which bypasses the
timed reachability analysis step. Instead, our method relies on
the reachability graph of the underlying untimed Petri~net. We
show that our approach is competitive for the translation of a
wide class of TPNs to~TAs in comparison with previous
approaches, both with regard to the time required to perform the
translation, and with regard to the number of locations and
clocks of the produced~TA.}
}
@inproceedings{BKKL-tacas07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = {4424},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Grumberg, Orna and Huth, Michael},
acronym = {{TACAS}'07},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'07)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
and Leucker, Martin},
title = {Replaying Play in and Play out: Synthesis of Design Models
from Scenarios by Learning},
pages = {435-450},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tacas07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tacas07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BKKL-tacas07.ps},
doi = {10.1007/978-3-540-71209-1_33},
abstract = {This paper is concerned with bridging the
gap between requirements, provided
as a set of scenarios, and conforming design models. The~novel aspect
of our approach is to exploit learning for the synthesis of design
models. In particular, we present a procedure that infers a
message-passing automaton~(MPA) from a given set of positive and
negative scenarios of the systems behavior provided as message
sequence
charts~(MSCs). The~paper investigates which classes of regular MSC
languages and corresponding MPAs can (not) be learned, and presents a
dedicated tool based on the learning library LearnLib that supports
our approach.}
}
@inproceedings{CJP-fossacs07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = 4423,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Seidl, Helmut},
acronym = {{FoSSaCS}'07},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'07)},
author = {Comon{-}Lundh, Hubert and Jacquemard, Florent and
Perrin, Nicolas},
title = {Tree Automata with Memory, Visibility and Structural
Constraints},
pages = {168-182},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-fossacs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-fossacs07.pdf},
doi = {10.1007/978-3-540-71389-0_13},
abstract = {Tree automata with one memory have been introduced in~2001. They
generalize both pushdown (word) automata and the tree automata with
constraints of equality between brothers of Bogaert and Tison. Though it has a
decidable emptiness problem, the main weakness of this model is its lack of
good closure properties. We~propose a generalization of the visibly pushdown
automata of Alur and Madhusudan to a family of tree recognizers which carry
along their (bottom-up) computation an auxiliary unbounded memory with a tree
structure (instead of a symbol stack). In~other words, these recognizers,
called visibly Tree Automata with Memory~(VTAM) define a subclass of tree
automata with one memory enjoying Boolean closure properties. We show in
particular that they can be determinized and the problems like emptiness,
inclusion and universality are decidable for~VTAM. Moreover, we propose an
extension of VTAM whose transitions may be constrained by structural equality
and disequality tests between memories, and show that this extension preserves
the good closure and decidability properties. }
}
@inproceedings{LMO-fossacs07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = 4423,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Seidl, Helmut},
acronym = {{FoSSaCS}'07},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'07)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Oreiby, Ghassan},
title = {On the Expressiveness and Complexity of~{ATL}},
pages = {243-257},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-fossacs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-fossacs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMO-fossacs07.ps},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08-erratum.pdf},
doi = {10.1007/978-3-540-71389-0_18},
abstract = {ATL is a temporal logic geared towards the specification and
verification of properties in multi-agents systems. It allows to reason on the
existence of strategies for coalitions of agents in order to enforce a given
property. We prove that the standard definition of~ATL (built on modalities
{"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be completed in order to express the
duals of its modalities: it~is necessary to add the modality {"}Release{"}.
We~then precisely characterize the complexity of ATL model-checking when the
number of agents is not fixed. We prove that it is \(\Delta_{2}^{P}\) and
\(\Delta_{3}^{P}\)-complete, depending on the underlying multi-agent model
(ATS and CGS,~resp.). We also prove that~ATL\({}^{+}\) model-checking is
\(\Delta_{3}^{P}\)-complete over both models, even with a fixed number of
agents.}
}
@inproceedings{BLM-fossacs07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = 4423,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Seidl, Helmut},
acronym = {{FoSSaCS}'07},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'07)},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Model-Checking One-Clock Priced Timed Automata},
pages = {108-122},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-fossacs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-fossacs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLM-fossacs07.ps},
doi = {10.1007/978-3-540-71389-0_9},
abstract = {We consider the model of priced (a.k.a.~weighted) timed
automata, an extension of timed automata with cost information on both
locations and transitions. We prove that model-checking this class of models
against the logic~WCTL, CTL~with cost-constrained modalities, is
PSPACE-complete under the {"}single-clock{"} assumption. In~contrast, it~has been
recently proved that the model-checking problem is undecidable for this model
as soon as the system has three clocks. We also prove that the model-checking
of~WCTL becomes undecidable, even under this {"}single-clock{"} assumption. }
}
@article{DLN-icomp2006,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David},
title = {On the freeze quantifier in constraint~{LTL}: Decidability
and complexity},
pages = {2-24},
year = {2007},
month = jan,
volume = 205,
number = 1,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLN-icomp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLN-icomp06.pdf},
doi = {10.1016/j.ic.2006.08.003},
abstract = {Constraint LTL, a generalisation of LTL over Presburger
constraints, is often used as a formal language to specify the behavior of
operational models with constraints. The freeze quantifier can be part of the
language, as in some real-time logics, but this variable-binding mechanism is
quite general and ubiquitous in many logical languages (first-order temporal
logics, hybrid logics, logics for sequence diagrams, navigation logics, logics
with \(\lambda\)-abstraction,~etc.). We show that Constraint~LTL over the
simple domain~\(\langle\mathbb{N}, =\rangle\) augmented with the freeze
quantifier is undecidable which is a surprising result in view of the poor
language for constraints (only equality tests). Many versions of freeze-free
Constraint LTL are decidable over domains with qualitative predicates and our
undecidability result actually establishes \(\Sigma_{1}^{1}\)-completeness. On
the positive side, we provide complexity results when the domain is finite
({\scshape ExpSpace}-completeness) or when the formulae are flat in a sense
introduced in the paper. Our undecidability results are sharp
(\emph{i.e.}~with restrictions on the number of variables) and all our
complexity characterisations ensure completeness with respect to some
complexity class (mainly {\scshape PSpace} and {\scshape ExpSpace}).}
}
@article{DN-ijfcs07,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Demri, St{\'e}phane and Nowak, David},
title = {Reasoning about transfinite sequences},
year = 2007,
volume = {18},
number = {1},
pages = {87-112},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-ijfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-ijfcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-ijfcs07.ps},
doi = {10.1142/S0129054107004589},
abstract = {We introduce a family of temporal logics to specify the behavior
of systems with Zeno behaviors. We~extend linear-time temporal logic LTL to
authorize models admitting Zeno sequences of actions and quantitative temporal
operators indexed by ordinals replace the standard next-time and until
future-time operators. Our aim is to control such systems by designing
controllers that safely work on \(\omega\)-sequences but interact
synchronously with the system in order to restrict their behaviors. We show
that the satisfiability and model-checking for the logics working on
\(\omega^{k}\)-sequences is \textsc{expspace}-complete when the integers are
represented in binary, and pspace-complete with a unary representation. To do
so, we substantially extend standard results about LTL by introducing a new
class of succinct ordinal automata that can encode the interaction between the
different quantitative temporal operators. }
}
@inproceedings{BCD-stacs2007,
address = {Aachen, Germany},
month = feb,
year = 2007,
volume = 4393,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Thomas, Wolfgang and Weil, Pascal},
acronym = {{STACS}'07},
booktitle = {{P}roceedings of the 24th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'07)},
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune,
St{\'e}phanie},
title = {Associative-Commutative Deducibility Constraints},
pages = {634-645},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-stacs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-stacs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-stacs07.ps},
doi = {10.1007/978-3-540-70918-3_54},
abstract = {We consider deducibility constraints, which are equivalent to
particular Diophantine systems, arising in the automatic verification of
security protocols, in presence of associative and commutative symbols. We
show that deciding such Diophantine systems is, in general, undecidable. Then,
we consider a simple subclass, which we show decidable. Though the solutions
of these problems are not necessarily semi-linear sets, we show that there are
(computable) semi-linear sets whose minimal solutions are not too far from the
minimal solutions of the system. Finally, we consider a small variant of the
problem, for which there is a much simpler decision algorithm. }
}
@article{BBBR-fmsd06,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Bruy{\`e}re, V{\'e}ronique and Raskin, Jean-Fran{\c{c}}ois},
title = {On the optimal reachability problem on weighted timed
automata},
volume = 31,
number = 2,
year = 2007,
month = oct,
pages = {135-175},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBR-FMSD06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBR-FMSD06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBR-FMSD06.ps},
doi = {10.1007/s10703-007-0035-4},
abstract = {We study the cost-optimal reachability problem for weighted
timed automata such that positive and negative costs are allowed on edges
and locations. By~optimality, we mean an infimum cost as well as a
supremum cost. We show that this problem is PSPACE-complete. Our~proof
uses techniques of linear programming, and thus exploits an important
property of optimal runs : their time-transitions use a time which is
arbitrarily closed to an integer. We~then propose an extension of the
region graph, the weighted discrete graph, whose structure gives light on
the way to solve the cost-optimal reachability problem. We~also give an
application of the cost-optimal reachability problem in the context of
timed games.}
}
@article{BBS-arxiv05,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Baier, Christel and Bertrand, Nathalie and
Schnoebelen, {\relax Ph}ilippe},
title = {Verifying nondeterministic probabilistic channel
systems against {{\(\omega\)}}-regular linear-time
properties},
year = 2007,
volume = 9,
number = 1,
nopages = {},
month = dec,
url = {http://arxiv.org/abs/cs.LO/0511023},
pdf = {http://arxiv.org/pdf/cs.LO/0511023},
ps = {http://arxiv.org/ps/cs.LO/0511023},
doi = {10.1145/1297658.1297663},
abstract = {Lossy channel systems (LCS's) are systems of finite state processes that
communicate via unreliable unbounded fifo channels. We introduce NPLCS's,
a variant of LCS's where message losses have a probabilistic behavior
while the component processes behave nondeterministically, and study the
decidability of qualitative verification problems for \(\omega\)-regular
linear-time properties.\par
We show that ---in contrast to finite-state Markov decision processes---
the satisfaction relation for linear-time formulas depends on the type of
schedulers that resolve the nondeterminism. While the qualitative model
checking problems for the full class of history-dependent schedulers is
undecidable, the same questions for finite-memory schedulers can be
solved algorithmically. Additionally, some special kinds of reachability,
or recurrent reachability, qualitative properties yield decidable
verification problems for the full class of schedulers, which ---for this
restricted class of problems--- are as powerful as finite-memory
schedulers, or even a subclass of them.}
}
@article{DD-icomp06,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Demri, St{\'e}phane and D'Souza, Deepak},
title = {An automata-theoretic approach to constraint~{LTL}},
year = 2007,
pages = {380-415},
volume = 205,
number = 3,
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DD-icomp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DD-icomp06.pdf},
doi = {10.1016/j.ic.2006.09.006},
abstract = {We consider an extension of linear-time temporal logic~(LTL)
with constraints interpreted over a concrete domain. We~use a new
automata-theoretic technique to show pspace decidability of the logic for the
constraint systems \((\mathbb{Z}, <, =)\) and \((\mathbb{N}, <, =)\). Along
the way, we give an automata-theoretic proof of a result of [Ph.~Balbiani,
J.~Condotta, \textit{Computational complexity of propositional linear temporal logics
based on qualitative spatial or temporal reasoning}, 2002] when the constraint system
satisfies the completion property. Our decision procedures extend easily to
handle extensions of the logic with past-time operators and constants, as well
as an extension of the temporal language itself to monadic second order logic.
Finally we show that the logic becomes undecidable when one considers
constraint systems that allow a counting mechanism.}
}
@article{DrGa07tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Droste, Manfred and Gastin, Paul},
title = {Weighted automata and weighted logics},
year = 2007,
month = jun,
volume = 380,
number = {1-2},
pages = {69-86},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-13.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-13.ps},
doi = {10.1016/j.tcs.2007.02.055},
abstract = {Weighted automata are used to describe quantitative properties
in various areas such as probabilistic systems, image
compression, speech-to-text processing. The~behaviour of
such an automaton is a mapping, called a formal power
series, assigning to each word a weight in some semiring.
We~generalize B{\"u}chi's and Elgot's fundamental theorems to this
quantitative setting. We~introduce a weighted version of MSO
logic and prove that, for commutative semirings, the
behaviours of weighted automata are precisely the formal
power series definable with particular sentences of our
weighted logic. We~also consider weighted first-order logic
and show that aperiodic series coincide with the first-order
definable ones, if the semiring is locally finite,
commutative and has some aperiodicity property.},
oldnote = {Special issue of ICALP'05. To appear.
Also available as Research Report LSV-05-13,
Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan,
France, July 2005.}
}
@article{LLT-icomp07,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
title = {Intruder Deduction for the Equational Theory of {A}belian Groups with
Distributive Encryption},
year = 2007,
volume = 205,
number = 4,
pages = {581-623},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-icomp07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-icomp07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LLT-icomp07.ps},
doi = {10.1016/j.ic.2006.10.008},
abstract = {Cryptographic protocols are small programs which involve a high
level of concurrency and which are difficult to analyze by hand. The~most
successful methods to verify such protocols are based on rewriting
techniques and automated deduction in order to implement or mimic the
process calculus describing the execution of a protocol. We~are interested
in the intruder deduction problem, that is vulnerability to passive attacks
in presence of equational theories which model the protocol specification
and properties of the cryptographic operators.\par
In the present paper we consider the case where the encryption distributes
over the operator of an Abelian group or over an exclusive-or
operator. We~prove decidability of the intruder deduction problem in both
cases. We~obtain a PTIME decision procedure in a restricted case, the
so-called binary case.\par
These decision procedures are based on a careful analysis of the proof
system modeling the deductive power of the intruder, taking into account the
algebraic properties of the equational theories under consideration.
The~analysis of the deduction rules interacting with the equational theory
relies on the manipulation of \(\mathbb{Z}\)-modules in the general case,
and on results from prefix rewriting in the binary case.}
}
@book{TATA07,
author = {Comon{-}Lundh, Hubert and Dauchet, Max and Gilleron, R{\'e}mi and
L{\"o}ding, Cristof and Jacquemard, Florent and
Lugiez, Denis and Tison, Sophie and Tommasi, Marc},
title = {Tree Automata Techniques and Applications},
year = 2007,
month = nov,
url = {http://www.grappa.univ-lille3.fr/tata/},
nmhowpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
nmnote = {release October, 12th 2007}
}
@misc{dots-rapp-6m,
author = {Fran{\c{c}}ois Laroussinie and others},
title = {Projet DOTS (ANR-06-SETI-003)~: Rapport {\`a} \(6\)~mois},
year = 2007,
month = aug,
type = {Contract Report},
note = {7~pages}
}
@misc{hcl:lecture07,
author = {Comon{-}Lundh, Hubert},
title = {Soundness of abstract cryptography},
oldhowpublished = {Lecture notes, part 1.
Available at \url{http://staff.aist.go.jp/h.comon-lundh/}},
year = {2007},
note = {Course notes (part~1), Symposium on Cryptography and
Information Security (SCIS2008), Tokai, Japan},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-sac08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-sac08.pdf}
}
@unpublished{JLC-rc,
author = {Carr{\'e}, Jean-Loup},
title = {R{\'e}{\'e}criture, confluence},
year = {2007},
month = dec,
note = {Course notes, {P}r{\'e}paration {\`a} l'agr{\'e}gation,
ENS Cachan, France}
}
@misc{averiles07-f1.6,
author = {Ourghanlian, Alain and Bozga, Marius and Roglewicz, Adam and
Sangnier, Arnaud},
title = {Projet {RNTL} {A}veriles~-- Fourniture F1.6~: Exp{\'e}rimentation},
year = 2007,
month = sep,
type = {Contract Report},
note = {16~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f16.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f16.pdf}
}
@misc{averiles07-f1.4,
author = {LIAFA and LSV and Verimag},
title = {Projet {RNTL} {A}veriles~-- Fourniture F1.4~: Prototypes d'outil},
year = 2007,
month = sep,
type = {Contract Report},
note = {3~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f14.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f14.pdf}
}
@misc{averiles07-f1.3,
author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
title = {Projet {RNTL} {A}veriles~-- Fourniture F1.3~: Algorithmes de v{\'e}rification},
year = 2007,
month = sep,
type = {Contract Report},
note = {19~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f13.pdf}
}
@misc{averiles07-f1.2,
author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
title = {Projet {RNTL} {A}veriles~-- Fourniture F1.2~: Extraction de mod{\`e}les},
year = 2007,
month = sep,
type = {Contract Report},
note = {19~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f12.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f12.pdf}
}
@misc{averiles07-f1.1,
author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
title = {Projet {RNTL} {A}veriles~-- Fourniture F1.1~: Mod{\`e}les},
year = 2007,
month = sep,
type = {Contract Report},
note = {6~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f11.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f11.pdf}
}
@misc{averiles07,
author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
title = {Rapport {\`a} mi-parcours du projet {RNTL} {A}veriles (analyse et
v{\'e}rification de logiciels embarqu{\'e}s avec structures
de m{\'e}moire dynamique},
year = 2007,
month = sep,
type = {Contract Report},
note = {4~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-MP.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-MP.pdf}
}
@unpublished{PG-algo,
author = {Gastin, Paul},
title = {Algorithmique},
year = {2007},
month = nov,
note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@unpublished{PG-languages,
author = {Gastin, Paul},
title = {Langages formels},
year = {2007},
month = may,
note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@misc{ltl2ba-v1.1,
author = {Gastin, Paul and Oddoux, Denis},
title = {LTL2BA~v1.1},
year = {2007},
month = aug,
nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/},
note = {Written in~C++ (about 4000 lines)},
note-fr = {\'Ecrit en~C++ (environ 4000 lignes)},
url = {http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/}
}
@misc{pronobis-final,
author = {ARC ProNoBis},
title = {ProNoBis: Probability and Nondeterminism, Bisimulations and
Security~-- {R}apport Final},
year = 2007,
month = oct,
type = {Contract Report},
nonote = {78~slides},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/pronobis-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/pronobis-final.pdf}
}
@misc{netqi-v1,
author = {Bursztein, Elie},
title = {NetQi~v1rc1},
year = {2007},
month = dec,
howpublished = {Available at \url{http://www.netqi.org/}},
note = {Written in~C and Java (about 10000 lines)},
note-fr = {\'Ecrit en~C et en Java (environ 10000 lignes)},
url = {http://www.netqi.org}
}
@inproceedings{SC-fcc07,
address = {Venice, Italy},
month = jul,
year = 2007,
editor = {Backes, Michael and Lakhnech, Yassine},
acronym = {{FCC}'07},
booktitle = {{P}roceedings of the 3rd {W}orkshop on {F}ormal and
{C}omputational {C}ryptography ({FCC}'07)},
author = {Steel ,Graham and Courant, Judica{\"e}l},
title = {A formal model for detecting parallel key search attacks},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-fcc07.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-fcc07.pdf}
}
@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.",
}}
@misc{GL:ARC-ProNoBis-16,
author = {Goubault-Larrecq, Jean},
howpublished = {Rapport final ARC ProNoBis},
month = oct,
title = {{Pronobis: Probability and nondeterminism,
bisimulations and security}},
year = {2007}
}
This file was generated by bibtex2html 1.98.