• On Unique Decomposition of Processes in the Applied Pi-Calculus.
  Jannik Dreier, Cristian Ene, Pascal Lafourcade and Yassine Lakhnech. FOSSACS 2013.
• Formal Verification of e-Auction protocols.
  Jannik Dreier, Pascal Lafourcade and Yassine Lakhnech. POST 2013.

• Generic Indiffirentiability Proofs for Hash Designs.
  M. Daubignard, P.-A. Fouque and Y. Lakhnech. CSF 2012 - In 25th IEEE Computer Security Foundations Symposium..
• Defining Privacy for Weighted Votes, Single and Multi-voter Coercion.
  J. Dreier, P. Lafourcade and Y. Lakhnech. ESORICS 2012.
• Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs (invited paper).
  G. Barthe, B. Grégoire, C. Kunz, Y. Lakhnech and S. Zanella Béguelin. Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012.
• A formal taxonomy of privacy in voting protocols.
  J. Dreier, P. Lafourcade and Y. Lakhnech. First IEEE International Workshop on Security and Forensics in Communication Systems (ICC'12 WS - SFCS), 2012
• Sécuriser les systèmes distribués à base de composants par contrôle de flux d'information.
  L. Sfaxi, T. Abdellatif, Y. Lakhnech et R. Robbana. TSI 2012.

• Computationally Sound Analysis of Encrypting with Diffie Hellman Keys.
  E. Bresson, Y. Lakhnech, L. Mazare, B. Warinschi.
  Chapter in Formal Models and Techniques for Analyzing Security Protocols. Veronique Cortier, Steve Kremer, (eds.). IOS Press.

• A Computational Indistinguishability logic for the Bounded Storage Model.
  G. Barth, M. Duclos, and Y. Lakhnech. In Foundations and Practice of Security 2011.

• Vote-Independency: A powerful privacy notion for voting protocols.
  Y. Dreir, P. Lafourcade, and Y. Lakhnech. In Foundations and Practice of Security 2011.

• Beyond Provable Security: Verifiable IND-CCA Security of OAEP.
  Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, and Santiago Zanella-Béguelin. In RSA 2011.

• Automating Information Flow Control in Component-based Distributed Systems.
  T. Abdellatif, L. Sfaxi, R. Robbaba and Y. Lakhnech. The 14th International ACM SIGSOFT Symposium on Component Based Software Engineering (CBSE-2011).

• Information Flow Control of Component-based Distributed Systems.
  T. Abdellatif, L. Sfaxi, R. Robbaba and Y. Lakhnech. Concurrency and Computation, Practice and Experience, Wiley

• Automated Proofs for Asymmetric Encryption.
  J. Courant, M. Daubignard, C. Ene, P. Lafourcade, Y. Lakhnech. In Journal of Automated Reasoning (3 July 2010)

• Computational Indistinguishability Logic.
  Gilles Barthe, Marion Daubignard, Bruce Kapron and Yassine Lakhnech. In ACM Conference on Computer and Communications Security 2010.

• Deciding equality of probabilistic terms.
  Gilles Barthe, Bruce Kapron, Yassine Lakhnech, and Vincent Laporte. In Proceedings of LPAR'10, Lecture Notes in Computer Science. Springer-Verlag, 2010.

• Automated Proofs for Asymmetric Encryption.
  Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech. In Concurrency, Compositionality, and Correctness LNCS 5930, 2010: 300-321. Essays in Honor of Willem-Paul de Roever.

• Formal Indistinguishability Extended to the Random Oracle Models.
  Cristian Ene, Yassine Lakhnech and Van Chan Ngo. ESORICS 2009: p. 555-570.

• Automated Proofs for Encryption Modes.
  Martin Gagné, Pascale Lafourcade, Yassine Lakhnech and Reihaneh Safavi-Naini. In ASIAN'09.

• Parametric Flat Counter Automata. Radu Iosif, Yassine Lakhnech and Marius Bozga. In Fundamenta Informaticae. Vol 91(2), p. 275-303, 2009.

• Towards Automated Proofs for Asymmetric Encryption in the Random Oracle Model. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech. In ACM Conference on Computer and Communications Security 2008: 371-380
• Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech. In FCS-ARSPA-WITS'08.
• Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech. IN FCC'08.

• A generalization of DDH with applications to protocol analysis and computational soundness . Emmanuel Bresson, Yassine Lakhnech, Laurent Mazaré and Bogdan Warinschi. In CRYPTO 2007.
• Computationally sound typing for Non-Interference: The case of deterministic encryption . Judicaël Courant, Cristian Ene and Yassine Lakhnech. In FSTTCS 2007.

• Flat Parametric Counter Automata.  M. Bozga, R. Iosif and Y. Lakhnech. Proc. Intl. Conference on Automata, Languages and Programming (ICALP 2006). Extended version appeared as VERIMAG TR 2005-15 .
• Game-based Criterion Partition Applied to Computational Soundness of Adaptive Security . Marion Daubignard, Romain Janvier, Yassine Lakhnech and Laurent Mazaré. International Workshop on Formal Aspects in Security and Trust (FAST'06), Hamilton, Canada, August 2006.
• Relating the Symbolic and Computational Models of Security Protocols Using Hashes Romain Janvier, Yassine Lakhnech and Laurent Mazaré. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), Seattle, US, August 2006.
• Soundness of Symbolic Equivalence for Modular Exponentiation Yassine Lakhnech, Laurent Mazaré and Bogdan Warinschi.  The 2nd Workshop on Formal and Computational Cryptography (FCC'06), Venice, Italy, July 2006.

• Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. R. Janvier, Y. Lakhnech and L. Mazaré. A conference version is accepted at ESOP'05.

• (De)Compositions of Cryptographic Schemes and their Applications to Protocols. R. Janvier, Y. Lakhnech and L. Mazaré.
  
• Probabilistic Opacity for a Passive Adversary and its Application to Chaum's Voting Scheme. Y. Lakhnech and L. Mazaré.
• Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation. Y. Lakhnech and L. Mazaré.
• A symbolic decision procedure for cryptographic protocols with time stamps. L. Bozga, Y. Lakhnech and C. Ene. Accepted in Journal of Logic and Algebraic Programming. Technical Report (in pdf).
• Pattern-based Abstraction for Verifying Secrecy in Protocols. L. Bozga, Y. Lakhnech and M. Perin. Journal version accepted in STTT.
  

•  On the existence of an effective and complete inference system for cryptographic protocols. L. Bozga, C. Ene and Yassine Lakhnech. A conference version is accepted at FOSSACS'04.
• Pattern-based Abstraction for Verifying Secrecy in Protocols. L. Bozga, Y. Lakhnech and M. Perin. Technical report (in pdf). Complete version of the TACAS'03 paper.
• A symbolic decision procedure for cryptographic protocols with time stamps. L. Bozga, C. Ene, and Yassine Lakhnech. CONCUR'04.
  
• On Logic of Aliasing. M. Bozga, Y. Lakhnech and R. Iosif.  Technical Report (in pdf). A conference version is accepted at SAS'04.
• Completing the Picture: Soundness of Formal Encryption in the Presence of Active  Adversaries. R. Janvier, Y. Lakhnech and L. Mazare. Technical Report, October 2004. Pdf version. Postcript version.
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Yassine Lakhnech and Sergio Yovine (Eds.). Conference proceedings of Formats and FTRTFT'04. LNCS 3253. (link)
  

• Pattern-based Abstraction for Verifying Secrecy in Protocols. L. Bozga, Y. Lakhnech and M. Perin.  TACAS'03. LNCS 2619.
• Storeless Semantics and Alias Logic.   M. Bozga, R. Iosif and Y. Lakkhnech. ACM SIGPLAN 2003  Workshop on Partial Evaluation and Semantics  Based Program Manipulation  (PEPM) .
• Hermes: An Automatic Tool for the Verification of Secrecy in Security Protocols. L. Bozga, Y. Lakhnech and M. Perin. CAV'03. LNCS 2725.

• Iterating Transducers.   D.  Dams, Y. Lakhnech and M. Steffen. Iterating Transducers.  Journal of Logic and Algebraic Programming. 52-53: 109-127 (2002).
• Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. K. Baukus, Y. Lakhnech and K. Stahl. VMCAI 2002 : 317-330.

• Concurrency Verification: Introduction to Compositonal and Noncompositional Methods . 
Willem-Paul de Roever, Frank de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers.Cambridge  University Press, 2001. Publisher information for this book: UK site , US site
• Verification of Parameterized Protocols. K. Baukus, Y. Lakhnech and K. Stahl. Journal of Universal Computer Science, vol. 7, no. 2 (2001).
• Incremental Verification by Abstraction. Y. Lakhnech, S. Bensalem, S. Berezin and S. Owre.  A conference version  of this paper  appeared in  the proceedings of the  7th International Conference, TACAS 2001, LNCS 20031  Springer-Verlag.
• Iterating Transducers.   D.  Dams, Y. Lakhnech and M. Steffen. Iterating Transducers. Accepted in CAV'01.
• Analyzing Fair Parametric Extended Automata . A. Annichini, A. Bouajjani, Y. Lakhnech and M. Sighireanu.Accepted at SAS'01
• Networks of Processes with Parameterized State Space. K. Baukus, Y. Lakhnech, S. Bensalem, and K. Stahl.
Satellite Workshops, ICALP 2001, ENTCS, pp. 388-402, Crete, Greece, 2001.
• Verifying Untimed and Timed Aspects of the Experimental Batch Plant. Ralf Huuck, Ben Lukoschus and Yassine Lakhnech.
European Journal of Control, 7(4):400-415, September 2001.  Hermes Science Publishing. ISSN 0947-3580.

2000

• Abstracting WS1S Systems to Verify Prameterized Networks. K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. A conference version  of this paper  appeared in  the proceedings of the  6th International Conference, TACAS 2000, LNCS 1785,  Springer-Verlag.
• Verifying Universal Properties of Parameterized Networks. K. Baukus, Y. Lakhnech, and K. Stahl. Proceedings of FTRTFT 2000.
• A Transformational Approach for Generating Non-linear Invariants. S. Bensalem, M. Bozga, J.-C. Fernandez, L. Ghirvu and Y. Lakhnech. A conference version  of this paper  appeared in  the proceedings of the  7th International Conference, SAS 2000, LNCS 1824,  Springer-Verlag.

•  Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. P.A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl and Y. Lakhnech. A conference version of this paper appeared in theproceedings of CAV'99 LNCS 1633, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag.

• Automatic Generation of Invariants. S. Bensalem and Y. Lakhnech. In Formal Methods and System Design 15(1) pp 75-92 July 1999.

•   Divide, abstract and  model-check.   K. Baukus, Y. Lakhnech, K. Stahl, and M. Steffen. A conference version  of this paper  appeared in  the

LNCS 1680, Springer-Verlag, 1999.

• Computing Abstractions of Infinite State Systems Compositionally and Automatically(in pdf) .
S. Bensalem, Y Lakhnech and S. Owre. A conference version of this paper appears in the proceedings of CAV'98 which will be published as an LNCS, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag.
• InVeSt : A Tool for the Verification of Invariants (in pdf) . S. Bensalem, Y Lakhnech and S. Owre.
A conference version of this paper appears in the proceedings of CAV'98 which is published as an LNCS, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag. 1995

• Synthesizing Different Development Paradigms: Combining Top-Down with Botton-Up Reasoning About Distributed Systems. .
   J. Zwiers, U. Hannemann, Y. Lakhnech, and W.-P. de Roever. Published in: Foundations of Software Technology and
Theoretical Computer Science.Lecture Notes in Computer Science 1026, 1995.

• Temporal Logic for Stabilizing Systems. . Y. Lakhnech and M. Siegel. Published in: International Conference on Temporal Logic, ICTL 1997.1996

• Modular Completeness: Integrating the Reuse of Specified Software in Top-Down Program Development.
J. Zwiers, U. Hannemann, Y. Lakhnech, F. Stomp, and W.-P. de Roever. Published in: Formal Methods Europe, FME'96 Symposium.
Lecture Notes in Computer Science 1051, 1996.

• Powerful Techniques for the Automatic Generation of Invariants. . S. Bensalem, Y. Lakhnech, and H. Saidi.
Published in: In Computer Aided Verification, CAV'96. Lecture Notes in Computer Science 1102, 1996.

• Utilizing Static Analysis for Programmable Logic Controllers. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
ADPM 2000 - The 4th International Conference Automation of Mixed Processes: Hybrid Dynamic Systems.
• An Abstract Model For Sequential Function Charts. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
WODES 2000 special session ``Formal Models of PLCs''.
• Verification of Sequential Function Charts using SMV. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus. PDPTA 2000 special session on Formal Validation.
• Approaches to the Formal Verification of Hybrid Systems. S. Kowalewski, P. Herrmann, S.  Engell, H.  Krumm, H.  Treseler, Y. Lakhnech, R. , B. Lukoschus.
Special issue of ``at-Automatisierungstechnik'' on the DFG research program KONDISK.

Integrating Timed Condition/Event Systems and Timed Automata to the Verificatiion of Hybrid Systems. Journal of Parallel and Distributed Computing Practices 1998.

• Verification of Timed Condition Event Systems and the tool DISCES.

• Comparing Timed Condition/Event Systems and Timed Automata. Proc. of HART'97, Grenoble, LNCS 1201:81-86, Springer-Verlag, 1997.

• Combining a Computer Science and Control Theory Approach for the Verification of Hybrid Systems. Proc. of the WPDRTS'97, Vienna, 1997.
• Analyse zeitbewerteter Bedingung/Ereignis-Systeme mittels Echtzeitautomaten-Tools. Proc. of the EKA'97, Braunschweig, 1997.
• Using Model-Checking for Timed Automata to Parameterize Logic Control Programs.8th European Symposium on Computer Aided Engineering, Brugge, Belgium, 1997.

• Ahmed Bouajjani, Yassine Lakhnech and Sergio Yovine.Model Checking for Extended Timed Temporal Logics . FTRTFT'96. Lecture Notes in Computer Science 1135, 1996.

• Yassine Lakhnech and Jozef Hooman. Metric Temporal Logic with Durations . Published in:Theoretical Computer Science 138, 1995.
• Ahmed Bouajjani, Yassine Lakhnech, and Riadh Robbana.From Duration Calculus to Hybrid Automata . Published in: Proceedings of the 7th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science 939, pp. 196--210, 1995.
• Ahmed Bouajjani and Yassine Lakhnech. Logics vs. Automata: The Hybrid Case . Published in: Hybrid Systems Workshop DIMACS'95, Lecture Notes in Computer Science 1066, 1995.

Ahmed Bouajjani and Yassine Lakhnech. Timed Automata + Temporal Logic: Expressiveness and Decidability . Published in: Proceedings of the 6th CONCUR'95: Concurrency Theory, Lecture Notes in Computer Science 962, pp. 531--546, 1995.

• Yassine Lakhnech and Jozef Hooman. Reasoning about durations in metric temporal logic . Published in: Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pp. 488--510, 1994.

• E. Mikk, Y. Lakhnech, C. Petersohn, and M. Siegel. On formal semantics of Statecharts as supported by STATEMATE . In 2nd BCS-FACS Northern Formal Methods Workshop. Springer-Verlag, July 97.
• E. Mikk, Y. Lakhnech, and M. Siegel.Hierarchical automata as model for statecharts.In Asian Computing Science Conference (ASIAN'97), volume 1345 of LNCS. Springer Verlag, December 97.
• E. Mikk, Y. Lakhnech, M. Siegel, and G. J. Holzmann. Implementing Statecharts in Promela/SPIN. In proceedings of WIFT98.
  

  ---

• HERMES : A Tool for the Verification of Cryptographic Protocols

• The PAX Tool: Verification of parameterized networks(not maintained)

• MOCES: A tool set for StateCharts (not maintained)

• InVeSt (not maintained)