---------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: July 2, 2009 (Brasilia, Brazil) Chair: Juergen Giesl Secretary: Peter Schneider-Kamp 19 Participants: Mauricio Ayala Rincon (invited) Dan Dougherty Maribel Fernandez Juergen Giesl Bernhard Gramlich Jean-Pierre Jouannaud Deepak Kapur Claude Kirchner Helene Kirchner Chris Lynch Aart Middeldorp Georg Moser (invited) Albert Rubio (invited) Manfred Schmidt-Schauss Peter Schneider-Kamp Ralf Treinen Roel de Vrijer (representing Vincent van Oostrom) Johannes Waldmann Hans Zantema ---------------------------------------------------------------------- Agenda: 1. Technical Presentations 2. International School on Rewriting (ISR) 3. Business Meeting ---------------------------------------------------------------------- 1. Technical presentations * Georg Moser: Complexity Analysis of Term Rewrite Systems In order to assess the complexity of a (terminating) TRS it is natural to look at the maximal length of derivations. Roughly such an analysis is conceivable as a worst-case complexity analysis of the functions computed by the given TRS. In the talk I will review well-established results in this area, but also present recent results on automatable techniques that verify that the given TRS admits at most polynomial (in the size of the start term) lengths of derivations. * Chris Lynch: Cap Unification: Application to Protocol Security modulo Homomorphic Encryption We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion (i.e., whether a secret term can be derived, possibly via interaction with the honest participants of the protocol) is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be employed in a simple manner to detect attacks exploiting some properties of block ciphers. This is joint work with Siva Anantharaman, Hai Lin, Paliath Narendran and Michael Rusinowitch. * Maribel Fernandez: A Rewriting Framework for the Composition of Access Control Policies In distributed environments where access control information may be shared across multiple sites, individual access control specifications need to be combined in order to define a coherent global policy. In order to ensure non-ambiguous behaviour, formal languages, often relying on first-order logic, have been developed for the description of access control policies. We propose a formalisation of policy composition by means of term rewriting. We will describe how, in this setting, we can express a wide range of policy combinations and reason about them. Modularity properties of rewrite systems will be used to derive the correctness of the global policy, i.e., that every access request has an answer and this answer is unique. * Albert Rubio: SMT in Termination In this talk we show that the use of SAT Modulo Theories (SMT) techniques for developing polynomial constraint solvers outperforms the best existing solvers. Moreover, we will see that the SMT framework provides a new and powerful approach for implementing better and more general solvers for termination provers. * Johannes Waldmann: SMT Solvers for Termination Provers To prove termination via interpretations, one needs coefficients of polynomials or matrices. The compatibility of the interpretation with the rewrite system is expressed as a constraint system. We will review some constraint languages available in the SMT (Satisfiability Modulo Theory) framework, give typical encodings, and evaluate the performance of current SMT solvers on those problems. We compare with "homegrown bitblasting", that is, encoding integer numbers in binary and translating to a Boolean satisfiability problem. This seems to be the method of choice for current termination provers. These experiments may lead to a more modular design of termination provers (by factoring out the constraint solvers), and help to connect the SMT and termination communities. ---------------------------------------------------------------------- 2. International School on Rewriting (ISR) * Mauricio Ayala Rincon: Report on ISR 2009 A report on the International Summer School on Rewriting in Brasilia (Brazil) preceding RDP 2009 was given. Most participants (19 out of 25) were from Brazil. The 6 other participants came from Mexico (2), Spain, Japan, and the United Kingdom. After the report, the working group discussed the following questions: What feedback is there from students? - Mauricio Ayala Rincon says they are enthusiastic (anecdotal evidence: Some students asked Franz Baader to sign his book on term rewriting). What feedback is there from lecturers? - Students seemed to have backgrounds in higher-order rewriting and lambda calculus rather than standard first-order rewriting. - The introductory track was rather long not giving much chance for students to really get accustomed with deeper topics in rewriting. - Students were mostly regional master students and shy with feedback. - Maribel Fernandez believes there will be a great impact to RTA as new students have been exposed to rewriting topics rather than existing PhD students already part of some rewriting groups. - Flavio de Moura states that the date of the last week of the semester was unfortunate as some students could not concentrate fully on ISR. * Juergen Giesl: Proposal for Changes of ISR Bylaws As decided at the previous IFIP WG 1.6 meeting, a proposal for changes of the ISR bylaws was prepared by Juergen Giesl and Aart Middeldorp. Juergen Giesl presented the changes, which can be summarized as follows: - The number of steering committee members is fixed to 6. - The steering committee members are the organizers of current, past, and future ISRs. - When a new organizer joins the steering committee, then a member with maximum serving time has to leave. - For complementing the currently only 4 such organizers, 2 members of the old steering committee should be appointed. The proposal was accepted unanimously after a short discussion. For the initial steering committee, J. Giesl and C. Lynch are appointed together with the current, past, and future organizers C. Kirchner, A. Middeldorp, M. Ayala Rincon, and V. van Oostrom. * Roel de Vrijer: Presentation on ISR 2010 The following information was presented: * R. de Vrijer will support the main organizer V. van Oostrom. * ISR 2010 will be a part of the Summer School Utrecht: http://www.utrechtsummerschool.nl/. The standing organizing committee of the Summer School Utrecht takes care of all logistics. * The proposed dates are Monday, July 5 - Friday, July 9. * The dates are restricted to be after July 2 (Utrecht semester). * 40 students (15 national, 25 international) are expected. * Housing on the campus ground should be around EUR 200 per week. * The organizers try to obtain funding from Utrecht University, Dutch research schools, and other organizations. * The structure of ISR 2010 will follow the one of ISR 2008 (a basic and an advanced track). Feedback on the presentation and proposed organization of ISR 2010: - Students and lecturers should be housed on campus if possible. - There are problems with the date (overlap with ICALP & FLoC workshops starting on July 9). ISR should be moved 1 or 2 days. - The registration fee of approx. EUR 600 excluding meals is felt to be too high. Costs for lecturers should probably be cut in order to increase participation of students. ---------------------------------------------------------------------- 3. Business meeting * Next meeting of the IFIP working group: There was consensus that the next IFIP WG 1.6 meeting should take place on July 10, 2010 as a pre-FLoC workshop in Edinburgh. * Inactive members: As decided at the previous meeting, all members were contacted and questioned w.r.t. their activity within the working group. Some people asked to leave the working group. There were 5 persons who did not respond and who can potentially be removed from the membership list to make room for new members. ----------------------------------------------------------------------