(boston lispers)

The Lisp Meeting will take place at MIT 34-401B.

Please note that the meeting is taking place not at NEU (like previous times) but at MIT (like the times before that). The location is confirmed - the same room as before at MIT. Please also note that the date is next week.

As the numbers indicate, this is in Building 34, on the 4th floor.

Maps: MIT Google

Many thanks go to Alexey Radul for arranging for the room, and to MIT for welcoming us.

ITA Software, a fine employer of Lisp hackers, is kindly purchasing a buffet to accompany our monthly Boston Lisp meeting. Anyone who attends is welcome to partake. We appreciate it if you let us know you're coming, and what food taboos you have, so that we can order the right amount of food. Tell us by sending email to boston-lisp-meeting-register at common-lisp.net. We won't send any acknowledgement unless requested; importantly, we'll keep your identity and address confidential and won't communicate any such information to anyone, not even to our sponsors.

Jay McCarthy will give a 25' talk about Cryptographic Protocol Explication and End-Point Projection.

Cryptographic protocols are useful for engineering trust in transactions. There are several languages for describing these protocols, but these tend to capture the communications from the perspective of an individual role. In contrast, traditional protocol descriptions as found in a state of nature tend to employ a whole-protocol description, resulting in an impedance mismatch.

In this talk we present two results to address this gap between human descriptions and deployable specifications. The first is an end-point projection technique that consumes an explicit whole-protocol description and generates specifications that capture the behavior of each participant role. In practice, however, many whole-protocol descriptions contain idiomatic forms of implicit specification. We therefore present our second result, a transformation that identifies and eliminates these implicit patterns, thereby preparing protocols for end-point projection.

Concretely, our tools consume protocols written in our whole-protocol language, WPPL, and generate role descriptions in the cryptographic protocol programming language, CPPL. We have formalized and established properties of the transformations using the Coq proof assistant. We have validated our transformations by applying them successfully to almost all the protocols in the SPORE repository.

This talk will be based off a paper co-authored that has been accepted at ESORICS, a joint work with Shriram Krisnamurthi.

Jay McCarthy is completing his PhD at Brown University under Shriram Krisnamurthi, and will be a professor of Computer Science next year at Brigham Young University.

---

There may or may not be a second speaker (to be announced), or some other community activity. Suggestions sought.