Yassine Lakhnech

93 papers A* 11A 8B 12C 2Journal 22Unranked 32

Year	Rank	Type	Title / Venue / Authors
2016	J	`jnl`	Automated Proofs of Block Cipher Modes of Operation. J. Autom. Reason. Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi-Naini
2016	J	`jnl`	On the existence and decidability of unique decompositions of processes in the applied π-calculus. Theor. Comput. Sci. Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
2015	—	`conf`	Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols. EUROCRYPT (2) Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt
2015	J	`jnl`	Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. IACR Cryptol. ePrint Arch. Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt
2014	—	`conf`	Formal Verification of e-Reputation Protocols. FPS Ali Kassem, Pascal Lafourcade, Yassine Lakhnech
2014	—	`ed.`	From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings FPS@ETAPS Saddek Bensalem, Yassine Lakhnech, Axel Legay
2013	—	`conf`	A More Realistic Model for Verifying Route Validity in Ad-Hoc Networks. FPS Ali Kassem, Pascal Lafourcade, Yassine Lakhnech
2013	A	`conf`	Automated Security Proofs for Almost-Universal Hash for MAC Verification. ESORICS Martin Gagné, Pascal Lafourcade, Yassine Lakhnech
2013	J	`jnl`	Automated Security Proofs for Almost-Universal Hash for MAC verification. IACR Cryptol. ePrint Arch. Martin Gagné, Pascal Lafourcade, Yassine Lakhnech
2013	C	`conf`	CIL Security Proof for a Password-Based Key Exchange. ProvSec Cristian Ene, Clémentine Gritti, Yassine Lakhnech
2013	—	`conf`	Formal Verification of e-Auction Protocols. POST Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech
2013	A*	`conf`	Fully automated analysis of padding-based encryption in the computational model. CCS Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Béguelin
2013	J	`jnl`	Information flow control of component-based distributed systems. Concurr. Comput. Pract. Exp. Lilia Sfaxi, Takoua Abdellatif, Riadh Robbana, Yassine Lakhnech
2013	B	`conf`	On Unique Decomposition of Processes in the Applied π-Calculus. FoSSaCS Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
2012	—	`conf`	A formal taxonomy of privacy in voting protocols. ICC Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech
2012	J	`jnl`	Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptol. ePrint Arch. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
2012	B	`conf`	Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. CPP Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
2012	A	`conf`	Defining Privacy for Weighted Votes, Single and Multi-voter Coercion. ESORICS Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech
2012	A	`conf`	Generic Indifferentiability Proofs of Hash Designs. CSF Marion Daubignard, Pierre-Alain Fouque, Yassine Lakhnech
2012	J	`jnl`	Sécuriser les systèmes distribués à base de composants par contrôle de flux d'information. Tech. Sci. Informatiques Lilia Sfaxi, Takoua Abdellatif, Yassine Lakhnech, Riadh Robbana
2011	—	`conf`	A Computational Indistinguishability Logic for the Bounded Storage Model. FPS Gilles Barthe, Mathilde Duclos, Yassine Lakhnech
2011	J	`jnl`	Automated Proofs for Asymmetric Encryption. J. Autom. Reason. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
2011	—	`conf`	Automated Verification of Block Cipher Modes of Operation, an Improved Method. FPS Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi-Naini
2011	—	`conf`	Automating information flow control in component-based distributed systems. CBSE Takoua Abdellatif, Lilia Sfaxi, Riadh Robbana, Yassine Lakhnech
2011	B	`conf`	Beyond Provable Security Verifiable IND-CCA Security of OAEP. CT-RSA Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
2011	B	`conf`	Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. CPP Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech
2011	—	`ch.`	Computational Soundness - The Case of Diffie-Hellman Keys. Formal Models and Techniques for Analyzing Security Protocols Emmanuel Bresson, Yassine Lakhnech, Laurent Mazaré, Bogdan Warinschi
2011	—	`conf`	Vote-Independence: A Powerful Privacy Notion for Voting Protocols. FPS Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech
2010	—	`conf`	Automated Proofs for Asymmetric Encryption. Concurrency, Compositionality, and Correctness Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
2010	A*	`conf`	Computational indistinguishability logic. CCS Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech
2010	—	`conf`	On the Equality of Probabilistic Terms. LPAR (Dakar) Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte
2009	—	`conf`	Automated Security Proof for Symmetric Encryption Modes. ASIAN Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi-Naini
2009	J	`jnl`	Flat Parametric Counter Automata. Fundam. Informaticae Marius Bozga, Radu Iosif, Yassine Lakhnech
2009	A	`conf`	Formal Indistinguishability Extended to the Random Oracle Model. ESORICS Cristian Ene, Yassine Lakhnech, Van Chan Ngo
2008	A*	`conf`	Towards automated proofs for asymmetric encryption schemes in the random oracle model. CCS Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
2007	A*	`conf`	A Generalization of DDH with Applications to Protocol Analysis and Computational Soundness. CRYPTO Emmanuel Bresson, Yassine Lakhnech, Laurent Mazaré, Bogdan Warinschi
2007	—	`conf`	Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption. FSTTCS Judicaël Courant, Cristian Ene, Yassine Lakhnech
2006	J	`jnl`	Certifying cryptographic protocols by abstract model-checking and proof concretization. SIGBED Rev. Romain Janvier, Yassine Lakhnech, Michaël Périn
2006	—	`conf`	Computational Soundness of Symbolic Analysis for Protocols Using Hash Functions. ICS@SYNASC Romain Janvier, Yassine Lakhnech, Laurent Mazaré
2006	—	`conf`	Flat Parametric Counter Automata. ICALP (2) Marius Bozga, Radu Iosif, Yassine Lakhnech
2006	—	`conf`	Game-Based Criterion Partition Applied to Computational Soundness of Adaptive Security. Formal Aspects in Security and Trust Marion Daubignard, Romain Janvier, Yassine Lakhnech, Laurent Mazaré
2006	J	`jnl`	Pattern-based abstraction for verifying secrecy in protocols. Int. J. Softw. Tools Technol. Transf. Liana Bozga, Yassine Lakhnech, Michaël Périn
2005	J	`jnl`	(De)Compositions of Cryptographic Schemes and their Applications to Protocols. IACR Cryptol. ePrint Arch. Romain Janvier, Yassine Lakhnech, Laurent Mazaré
2005	J	`jnl`	A symbolic decision procedure for cryptographic protocols with time stamps. J. Log. Algebraic Methods Program. Liana Bozga, Cristian Ene, Yassine Lakhnech
2005	—	`conf`	Automatic Verification of Security Properties Based on Abstractions. VISSAS Liana Bozga, Cristian Ene, Romain Janvier, Yassine Lakhnech, Laurent Mazaré, Michaël Périn
2005	A	`conf`	Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. ESOP Romain Janvier, Yassine Lakhnech, Laurent Mazaré
2005	J	`jnl`	Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation. IACR Cryptol. ePrint Arch. Yassine Lakhnech, Laurent Mazaré
2005	J	`jnl`	Guidelines for a graduate curriculum on embedded software and systems. ACM Trans. Embed. Comput. Syst. Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Luís Almeida, Albert Benveniste, Bruno Bouyssounouse, Giorgio C. Buttazzo, Ivica Crnkovic, Werner Damm, Jakob Engblom, Gerhard Fohler, Marisol García-Valls, Hermann Kopetz, Yassine Lakhnech, François Laroussinie, Luciano Lavagno, Giuseppe Lipari, Florence Maraninchi, Philipp Peti, Juan Antonio de la Puente, Norman Scaife, Joseph Sifakis, Robert de Simone, Martin Törngren, Paulo Veríssimo, Andy J. Wellings, Reinhard Wilhelm, Tim A. C. Willemse, Wang Yi
2005	J	`jnl`	Probabilistic Opacity for a Passive Adversary and its Application to Chaum's Voting Scheme. IACR Cryptol. ePrint Arch. Yassine Lakhnech, Laurent Mazaré
2004	B	`conf`	A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract). CONCUR Liana Bozga, Cristian Ene, Yassine Lakhnech
2004	—	`ed.`	Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings FORMATS/FTRTFT Yassine Lakhnech, Sergio Yovine
2004	B	`conf`	On Logics of Aliasing. SAS Marius Bozga, Radu Iosif, Yassine Lakhnech
2004	B	`conf`	On the Existence of an Effective and Complete Inference System for Cryptographic Protocols. FoSSaCS Liana Bozga, Cristian Ene, Yassine Lakhnech
2003	—	`conf`	Abstraction as the Key for Invariant Verification. Verification: Theory and Practice Saddek Bensalem, Susanne Graf, Yassine Lakhnech
2003	A*	`conf`	HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. CAV Liana Bozga, Yassine Lakhnech, Michaël Périn
2003	A	`conf`	Pattern-Based Abstraction for Verifying Secrecy in Protocols. TACAS Liana Bozga, Yassine Lakhnech, Michaël Périn
2003	C	`conf`	Storeless semantics and alias logic. PEPM Marius Bozga, Radu Iosif, Yassine Lakhnech
2002	J	`jnl`	Iterating transducers. J. Log. Algebraic Methods Program. Dennis Dams, Yassine Lakhnech, Martin Steffen
2002	B	`conf`	Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. VMCAI Kai Baukus, Yassine Lakhnech, Karsten Stahl
2001	B	`conf`	Analyzing Fair Parametric Extended Automata. SAS Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu
2001	—	`book`	Concurrency Verification: Introduction to Compositional and Noncompositional Methods Willem P. de Roever, Frank S. de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, Job Zwiers
2001	A	`conf`	Incremental Verification by Abstraction. TACAS Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre
2001	A*	`conf`	Iterating Transducers. CAV Dennis Dams, Yassine Lakhnech, Martin Steffen
2001	—	`conf`	Networks of Processes with Parameterized State Space. VEPAS Kai Baukus, Karsten Stahl, Saddek Bensalem, Yassine Lakhnech
2001	J	`jnl`	Verification of Parameterized Protocols. J. Univers. Comput. Sci. Kai Baukus, Yassine Lakhnech, Karsten Stahl
2001	J	`jnl`	Verifying Untimed and Timed Aspects of the Experimental Batch Plant. Eur. J. Control Ralf Huuck, Ben Lukoschus, Yassine Lakhnech
2000	B	`conf`	A Transformational Approach for Generating Non-linear Invariants. SAS Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Yassine Lakhnech
2000	A	`conf`	Abstracting WS1S Systems to Verify Parameterized Networks. TACAS Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl
2000	—	`conf`	Basic Principles of a textbook on the compositional and noncompositional verification of concurrent programs. FBT Willem P. de Roever, Frank S. de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, Job Zwiers
2000	—	`conf`	Verifying Universal Properties of Parameterized Networks. FTRTFT Kai Baukus, Yassine Lakhnech, Karsten Stahl
1999	J	`jnl`	Automatic Generation of Invariants. Formal Methods Syst. Des. Saddek Bensalem, Yassine Lakhnech
1999	—	`conf`	Divide, Abstract, and Model-Check. SPIN Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen
1999	—	`ed.`	Proceedings of the International Workshop Tool Support for System Specification, Development and Verification, Malente, Germany, June 1-4, 1998 Tool Support for System Specification, Development and Verification Rudolf Berghammer, Yassine Lakhnech
1999	A*	`conf`	Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. CAV Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech
1998	A*	`conf`	Computing Abstractions of Infinite State Systems Compositionally and Automatically. CAV Saddek Bensalem, Yassine Lakhnech, Sam Owre
1998	—	`conf`	Formal Methods and Tools: Introduction and Overview. Tool Support for System Specification, Development and Verification Rudolf Berghammer, Yassine Lakhnech, Wolfgang Reif
1998	—	`conf`	Implementing Statecharts in PROMELA/SPIN. WIFT Erich Mikk, Yassine Lakhnech, Michael Siegel, Gerard J. Holzmann
1998	A*	`conf`	InVeST: A Tool for the Verification of Invariants. CAV Saddek Bensalem, Yassine Lakhnech, Sam Owre
1998	J	`jnl`	Integrating Timed Condition/Event Systems and Timed Automata for the Verification of Hybrid Systems. Parallel Distributed Comput. Pract. Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jörg Preußig
1997	—	`conf`	Comparing Timed C/E Systems with Timed Automata (Abstract). HART Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jörg Preußig
1997	—	`conf`	Deductive verification of stabilizing systems. WSS Yassine Lakhnech, Michael Siegel
1997	—	`conf`	Hierarchical Automata as Model for Statecharts. ASIAN Erich Mikk, Yassine Lakhnech, Michael Siegel
1996	—	`conf`	Model-Checking for Extended Timed Temporal Logics. FTRTFT Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine
1996	—	`conf`	Modular Completeness: Integrating the Reuse of Specified Software in Top-down Program Development. FME Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, Willem P. de Roever, Frank A. Stomp
1996	A*	`conf`	Powerful Techniques for the Automatic Generation of Invariants. CAV Saddek Bensalem, Yassine Lakhnech, Hassen Saïdi
1996	—	`—`	Specification and verification of hybrid and real time systems. Yassine Lakhnech
1995	A*	`conf`	From Duration Calculus To Linear Hybrid Automata. CAV Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana
1995	—	`conf`	Logics vs. Automata: The Hybrid Case. Hybrid Systems Ahmed Bouajjani, Yassine Lakhnech
1995	J	`jnl`	Metric Temporal Logic with Durations. Theor. Comput. Sci. Yassine Lakhnech, Jozef Hooman
1995	—	`conf`	Synthesizing Different Development Paradigms: Combining Top-Down with Bottom-Up Reasoning About Distributed Systems. FSTTCS Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, Willem P. de Roever
1995	B	`conf`	Temporal Logic + Timed Automata: Expressiveness and Decidability. CONCUR Ahmed Bouajjani, Yassine Lakhnech
1994	—	`conf`	Reasoning about Durations in Metric Temporal Logic. FTRTFT Yassine Lakhnech, Jozef Hooman
1992	B	`conf`	Provably Correct Compiler Development and Implementation. CC Bettina Buth, Karl-Heinz Buth, Martin Fränzle, Burghard von Karger, Yassine Lakhnech, Hans Langmaack, Markus Müller-Olm