[TYPES/announce] Postdoc position: Symbolic tools for the formal verification of cryptographic protocols
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] A 12-month position for post-doctoral research on Symbolic tools for the formal verification of cryptographic protocols is available at the Inria Nancy / LORIA research center within the Inria project team PESTO: Proof techniques for security protocols [1] as part of the ERC Grant SPOOC: Automated Security Proofs of Cryptographic Protocols [2] Security protocols are distributed programs that aim at ensuring security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the Internet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness. One generally distinguishes two families of security properties: trace properties and observational equivalence properties. Trace properties verify a predicate on a given trace and are typically used to express authentication properties. Observational equivalence expresses that an adversary cannot distinguish two situations and is used to model anonymity and strong confidentiality properties. The Tamarin prover [3] is a state-of-the art protocol verification tool which has recently been extended to verify equivalence properties in addition to trace properties. SAPIC [4] allows protocols to be specified in a high-level protocol specification language, an extension of the applied pi-calculus, and uses the Tamarin prover as a backend by compiling the language into multi-set rewrite rules, the input format of Tamarin. Tamarin and SAPIC have been successfully used to verify standards such as TLS 1.3 and 5G AKA as well as industrial protocols such as OPC UA. The objective of this postdoc is to contribute to the development of the SAPIC/Tamarin toolchain, work on extensions and use the tool(s) to analyse particular classes of protocols. Successful candidates must have defended a PhD in computer science, or expect to defend their PhD before taking up the position. Expected qualifications are: - solid knowledge of logic, proofs and/or formal verification techniques, - solid programming experience, ideally with functional programming in OCAML or Haskell. Security knowledge is not required, but a plus. Contacts: Jannik Dreier (jannik.dre...@loria.fr) Steve Kremer (steve.kre...@loria.fr) Duration: 12 months (possibility to extend for another 12 months) Starting date: September 1, 2019 (earlier date negociable) The position is located at the Inria Nancy / LORIA research center in Nancy, France, with over 430 researchers, engineers and technicians. Nancy is a young (more than 45,000 students) city in eastern France with a rich cultural life and a high quality of life. It is famous for its Unesco World Heritage Site "Place Stanislas". Paris is only 1h30 by TGV, Luxembourg, Germany and the Vosges mountains less than 1h30 by car. Applications, including - a motivation letter including your scientific and career projects, - a CV describing your research activities (max. 2 pages), - a short description of your best contributions (max. 1 page for max. 3 contributions including theoretical research, implementation or industry transfer), - your two best publications, - if you have not defended yet, the list of expected members of your PhD committee and the expected date of defense, should be sent to the the addresses indicated above as two pdf files (one for the publications, the other for the other documents). Additionally, at least one recommendation letter from your PhD advisor(s), and up to two additional letters of recommendation should be sent directly by their authors to the email addresses indicated above. Applications should be received by June 30, 2019, but applications received later may still be considered. Informal enquiries concerning the position are welcome. [1] https://team.inria.fr/pesto/ [2] http://homepages.loria.fr/skremer/spooc/ [3] http://tamarin-prover.github.io/ [4] http://sapic.gforge.inria.fr/
[TYPES/announce] Final Call for Papers for POST 2014
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologize for crossposting] *** 3rd Conference on Principles of Security and Trust (POST 2014) (http://www.etaps.org/2014/post) A member conference of ETAPS. !! deadline for abstracts : 4 October 2013 !! !! deadline for full papers : 11 October 2013 !! *** Principles of Security and Trust is a broad forum related to the theoretical and foundational aspects of security and trust. Papers of many kinds are welcome: new theoretical results, practical applications of existing foundational ideas, and innovative theoretical approaches stimulated by pressing practical problems. POST was created in 2012 as one of the ETAPS (http://www.etaps.org/) main conferences to combine and replace a number of successful and longstanding workshops in this area: Automated Reasoning and Security Protocol Analysis (ARSPA), Formal Aspects of Security and Trust (FAST), Security in Concurrency (SecCo), and the Workshop on Issues in the Theory of Security (WITS). A subset of these events met jointly as an event affiliated with ETAPS 2011 under the name Theory of Security and Applications (TOSCA). POST'14 is the 3rd edition, following POST'12 in Tallinn, Estonia and POST'13 in Rome, Italy. We seek submissions proposing theories to clarify security and trust within computer science; submissions establishing new results in existing theories; and also submissions raising fundamental concerns about existing theories. We welcome new techniques and tools to automate reasoning within such theories, or to solve security and trust problems. Case studies that reflect the strengths and limitations of foundational approaches are also welcome, as are more exploratory presentations on open questions. Areas of interest include: * Access control * Anonymity * Authentication * Availability * Cloud security * Confidentiality * Covert channels * Crypto foundations * Economic issues * Information flow * Integrity * Languages for security * Malicious code * Mobile code * Models and policies * Privacy * Provenance * Reputation and trust * Resource usage * Risk assessment * Security architectures * Security protocols * Trust management * Web service security Important Dates Submission deadline for abstracts (strict): 4 October 2013 Submission deadline for full papers (strict): 11 October 2013 Notification of decision: 20 December 2013 Camera-ready versions due: 17 January 2014 Presentations in Grenoble, France: 7–11 April 2014 Submission Guidelines Papers submitted to POST have a page limit of 20 pages, including the bibliography. Additional material intended for the referees but not for publication in the final version - for example, details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. Referees are at liberty to ignore appendices and papers must be understandable without them. The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline Springer's Lecture Notes in Computer Science series. Other general submission information, including formatting guidelines, are available from the ETAPS 2014 common call for papers (http://www.etaps.org/2014/etaps-2014-common-call-for-papers). Papers must be submitted through the POST 2014 author interface of Easychair (https://www.easychair.org/conferences/?conf=post14). Invited speaker David Mazières (Stanford University, USA) Programme Chairs Martín Abadi (MSR Silicon Valley UCSC, USA) Steve Kremer (Inria Nancy, France) Programme Committee Anindya Banerjee (IMDEA, Spain) Bruno Blanchet (Inria Paris, France) Ran Canetti (Boston University, USA and Tel Aviv Univ. Israel) Claude Castelluccia (Inria Grenoble, France) George Danezis (MSR Cambridge, UK) Anupam Datta (CMU, USA) Stéphanie Delaune (ENS Cachan, France) Riccardo Focardi (University of Venice, Italy) Somesh Jha (University of Wisconsin, USA) Ninghui Li (Purdue University, USA) Sergio Maffeis (Imperial College, UK) Andrew Myers (Cornell University, USA) Catuscia Palamidessi (Inria Saclay, École Polytechnique, France) Benjamin Pierce (University of Pennsylvania, USA) Frank Piessens (KU Leuven, Belgium) David Pointcheval (ENS Paris, France) David Sands (Chalmers University of Technology, Sweden) Hovav Shacham (UCSD, USA) Nikhil Swamy (MSR Redmond, USA) Paul Syverson (NRL, USA) Ankur Taly (Google, USA) Bogdan Warinschi (Bristol University, UK)
[TYPES/announce] 3rd Conference on Principles of Security and Trust (POST 2014)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] *** Call for Papers 3rd Conference on Principles of Security and Trust (POST 2014) (http://www.etaps.org/2014/post-2014) *** Principles of Security and Trust is a broad forum related to the theoretical and foundational aspects of security and trust. Papers of many kinds are welcome: new theoretical results, practical applications of existing foundational ideas, and innovative theoretical approaches stimulated by pressing practical problems. POST was created in 2012 as one of the ETAPS (http://www.etaps.org/) main conferences to combine and replace a number of successful and longstanding workshops in this area: Automated Reasoning and Security Protocol Analysis (ARSPA), Formal Aspects of Security and Trust (FAST), Security in Concurrency (SecCo), and the Workshop on Issues in the Theory of Security (WITS). A subset of these events met jointly as an event affiliated with ETAPS 2011 under the name Theory of Security and Applications (TOSCA). POST'14 is the 3rd edition, following POST'12 in Tallinn, Estonia and POST'13 in Rome, Italy. We seek submissions proposing theories to clarify security and trust within computer science; submissions establishing new results in existing theories; and also submissions raising fundamental concerns about existing theories. We welcome new techniques and tools to automate reasoning within such theories, or to solve security and trust problems. Case studies that reflect the strengths and limitations of foundational approaches are also welcome, as are more exploratory presentations on open questions. Areas of interest include: * Access control * Anonymity * Authentication * Availability * Cloud security * Confidentiality * Covert channels * Crypto foundations * Economic issues * Information flow * Integrity * Languages for security * Malicious code * Mobile code * Models and policies * Privacy * Provenance * Reputation and trust * Resource usage * Risk assessment * Security architectures * Security protocols * Trust management * Web service security Important Dates Submission deadline for abstracts (strict): 4 October 2013 Submission deadline for full papers (strict): 11 October 2013 Notification of decision: 20 December 2013 Camera-ready versions due: 17 January 2014 Presentations in Grenoble, France: 7–11 April 2014 Submission Guidelines Papers submitted to POST have a page limit of 20 pages, including the bibliography. Additional material intended for the referees but not for publication in the final version - for example, details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. Referees are at liberty to ignore appendices and papers must be understandable without them. The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline Springer's Lecture Notes in Computer Science series. Other general submission information, including formatting guidelines, are available from the ETAPS 2014 common call for papers (http://www.etaps.org/2014/etaps-2014-common-call-for-papers). Papers must be submitted through the POST 2014 author interface of Easychair (https://www.easychair.org/conferences/?conf=post14). Invited speaker David Mazières (Stanford University, USA) Programme Chairs Martín Abadi (MSR Silicon Valley UCSC, USA) Steve Kremer (Inria Nancy, France) Programme Committee Anindya Banerjee (IMDEA, Spain) Bruno Blanchet (Inria Paris, France) Ran Canetti (Boston University, USA and Tel Aviv Univ. Israel) Claude Castelluccia (Inria Grenoble, France) George Danezis (MSR Cambridge, UK) Anupam Datta (CMU, USA) Stéphanie Delaune (ENS Cachan, France) Riccardo Focardi (University of Venice, Italy) Somesh Jha (University of Wisconsin, USA) Ninghui Li (Purdue University, USA) Sergio Maffeis (Imperial College, UK) Andrew Myers (Cornell University, USA) Catuscia Palamidessi (Inria Saclay, École Polytechnique, France) Benjamin Pierce (University of Pennsylvania, USA) Frank Piessens (KU Leuven, Belgium) David Pointcheval (ENS Paris, France) David Sands (Chalmers University of Technology, Sweden) Hovav Shacham (UCSD, USA) Nikhil Swamy (MSR Redmond, USA) Paul Syverson (NRL, USA) Ankur Taly (Google, USA) Bogdan Warinschi (Bristol University, UK)
[TYPES/announce] Information and Computation special issue on security and rewriting
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Special issue of Information and Computation on Security and Rewriting Techniques http://www.lsv.ens-cachan.fr/~kremer/secret-special-issue/ Call for Papers Scope: Rewriting Techniques in a broad sense, including for instance constraint solving techniques, logic programming and automata techniques, have been recently applied with success in various areas of security. Typical examples include security protocols, security policies, web services, and access control. We seek submissions of original research papers in these areas. They will be evaluated according to the high standards of Information and Computation and accepted papers will appear in a special issue of this journal. Submissions: Submissions, in pdf format, must be sent to the two guest editors by E-mail, no later than February 18, 2011 We encourage the use of Elsevier's elsarticle.cls latex macro package, that can be retrieved from http://www.elsevier.com/wps/find/authorsview.authors/elsarticle Editors: Steve Kremerkre...@lsv.ens-cachan.fr Paliath Narendran d...@cs.albany.edu Please send any further inquiry to any of the two above editors.
[TYPES/announce] SecReT 2010 Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] *** Call for Participation 5th International Workshop on Security and Rewriting Techniques (SecReT 2010) http://users.dsic.upv.es/workshops/secret2010/ Valencia (Spain), June 18-20. *** IMPORTANT INFORMATION Early registration deadline: June 6, 2010 INVITED SPEAKERS - Bruno Blanchet (LIENS, France) - Ralf Kuesters (Univ. Trier, Germany) - Catherine Meadows (NRL, USA) - Michaël Rusinowitch (INRIA, France) AIMS AND SCOPE We need to increase our confidence in security related applications. Formal verification is one of the most important methods of achieving this goal, and term rewriting has already played an important part. In particular, since the beginning of formal verification of security protocols, term rewriting has played a central role, both as a computation model and as a deduction strategy. Because of this, we believe that it can play an important role in solving other security-related formal verification problems as well. That is why it is important to bring together experts in term rewriting, constraint solving, equational reasoning on the one side and experts in security on the other side. This is precisely the aim of this workshop. A possible (non exhaustive) list of topics include application of rewriting or constraint solving to authentication, encryption, access control and authorization, protocol verification, specification and analysis of policies, intrusion detection, integrity of information, control of information leakage, control of distributed and mobile code, etc. ACCEPTED PAPERS Automating security analysis: symbolic equivalence of constraint systems Vincent Cheval, Hubert Comon-Lundh and Stephanie Delaune Deducibility constraints Sergiu Bursuc, Hubert Comon-Lundh and Stephanie Delaune Semi-Automatic Synthesis of Security Policies by Invariant-Guided Abduction Clément Hurlin and Helene Kirchner Efficient XOR Unification Zhiqiang Liu and Christopher Lynch Sequential Protocol Composition in Maude-NPA Santiago Escobar, Catherine Meadows, Jose Meseguer and Sonia Santiago Rule-based Specification and Analysis of Security Policies Tony Bourdier, Horatiu Cirstea, Mathieu Jaume and Helene Kirchner. Maude-NPA Tool Demo Santiago Escobar, Catherine Meadows and Jose Meseguer Automated Abstract Certification of Global Non-interference in Rewriting Logic Mauricio Alba-Castro, María Alpuente and Santiago Escobar Finitary Deduction Systems Yannick Chevalier and Mounira Kourjieh Geometric Logic and Strand Spaces Daniel Dougherty and Joshua Guttman Deciding trace equivalence for finite cryptographic process calculi Rohit Chadha, Stefan Ciobaca and Steve Kremer Abstractions for Verifying Key Management APIs Graham Steel PROGRAM COMMITTEE Yannick Chevalier (IRIT, Toulouse, France) Hubert Comon-Lundh (LSV, Cachan, France) Daniel Dougherty (WPI, Worcester, USA) Santiago Escobar (Univ. Politécnica Valencia, Spain) Steve Kremer (LSV, Cachan, France) - co-chair Christopher Lynch (Clarkson Univ., USA) José Meseguer (Univ. Illinois, USA) Paliath Narendran (SUNY Albany, USA) - co-chair
[TYPES/announce] SecReT 2010
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] 5th International Workshop on Security and Rewriting Techniques (SecReT 2010) Valencia (Spain), June 18-20. Aims and Scope: We need to increase our confidence in security related applications. Formal verification is one of the most important methods of achieving this goal, and term rewriting has already played an important part. In particular, since the beginning of formal verification of security protocols, term rewriting has played a central role, both as a computation model and as a deduction strategy. Because of this, we believe that it can play an important role in solving other security-related formal verification problems as well. That is why it is important to bring together experts in term rewriting, constraint solving, equational reasoning on the one side and experts in security on the other side. This is precisely the aim of this workshop. A possible (non exhaustive) list of topics include application of rewriting or constraint solving to authentication, encryption, access control and authorization, protocol verification, specification and analysis of policies, intrusion detection, integrity of information, control of information leakage, control of distributed and mobile code, etc. Submission instructions: The workshop will have no formal proceedings. We therefore encourage submission of ongoing work as well as recently published work. Submissions should be 1 page abstract summarizing the work the authors would like to present. Detailed submission instructions will soon be available on the workshop's website. Important dates: - Submission deadline: April 2 - Notification: April 23 - Workshop: June 18-20 Invited speakers: - Bruno Blanchet - Ralf Kuesters - Catherine Meadows - Michael Rusinowith Program Committee: - Yannick Chevalier - Hubert Comon-Lundh - Dan Dougherty - Santiago Escobar - Steve Kremer (co-chair) - Chris Lynch - Jose Meseguer - Paliath Narendran (co-chair)
[TYPES/announce] SecCo'09 CFP
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] _ | | |7th International Workshop on| | Security Issues in Concurrency | | | | (SecCo'09) | | http://www.lsv.ens-cachan.fr/Events/SecCo09/| |_| | | | September 5, 2009, Bologna (Italy) | | Affiliated to CONCUR 2009 | |_| SCOPE AND TOPICS: Emerging trends in concurrency theory require the definition of models and languages adequate for the design and management of new classes of applications, mainly to program either WANs (like Internet) or smaller networks of mobile and portable devices (which support applications based on a dynamically reconfigurable communication structure). Due to the openness of these systems, new critical aspects come into play, such as the need to deal with malicious components or with a hostile environment. Current research on network security issues (e.g. secrecy, authentication, etc.) usually focuses on opening cryptographic point-to-point tunnels. Therefore, the proposed solutions in this area are not always exploitable to support the end-to-end secure interaction between entities whose availability or location is not known beforehand. The aim of the workshop is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on common interests and stimulating discussions on central research questions. In particular, we look for papers dealing with security issues -- such as authentication, integrity, privacy, confidentiality, access control, denial of service, service availability, safety aspects, fault tolerance, trust, language-based security, probabilistic and information theoretic models -- in emerging fields like web services, mobile ad-hoc networks, agent-based infrastructures, peer-to-peer systems, context-aware computing, global/ubiquitous/pervasive computing. SecCo'08 follows the success of SecCo'03 (affiliated to ICALP'03), SecCo'04 (affiliated to CONCUR'04), SecCo'05 (affiliated to CONCUR'05), SecCo'07 (affiliated to CONCUR'07) and SecCo'08 (affiliated to CONCUR'08). INVITED SPEAKER - Riccardo Focardi (Universita Ca' Foscari, Italy) PROGRAMME COMMITTEE: * Michele Boreale, co-chair (Università di Firenze, Italy) * Gerard Boudol (INRIA, Sophia-Antipolis, France) * Mads Dam (KTH, Sweden) * Anupam Datta (Carnegie Mellon, USA) * Stephanie Delaune (LSV, ENS Cachan, France) * Joshua D. Guttman (MITRE Corporation, USA) * Steve Kremer, co-chair, (LSV, ENS Cachan, CNRS, INRIA, France) * Gavin Lowe (University of Oxford, UK) * Pasquale Malacaria (Queen Mary, London, UK) * Catuscia Palamidessi (INRIA Saclay and LIX , France) * Geoffrey Smith (Florida International University, USA) IMPORTANT DATES: * Deadline for paper submission: June 1 2009 * Notification: June 26 2009 * Workshop: September 5 2009 SUBMISSION GUIDELINES: The workshop proceedings will be published in the new EPTCS series (Electronic Proceedings in Theoretical Computer Science, see http://www.cse.unsw.edu.au/~rvg/EPTCS/); we thus encourage submissions already in that format. Submissions may be of two kinds: * Short papers (not included in the proceedings): up to 5 pages; * Full papers: up to 15 pages (including bibliography). Papers must be sumbitted electronically at the following URL: http://www.easychair.org/conferences/?conf=secco09 Simultaneous submission to other conferences or journals is only allowed for short papers. These are an opportunity to present innovative ideas (without working out a full paper) and to get feedback from a technically competent audience. As done for the previous SecCo workshops, if the quality of the accepted submissions warrants it, there will be a special issue of the Journal of Computer Security devoted to selected papers from the workshop.
