@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.*