Expi2Java 1.6 Released

May 13, 2011

Alex Busenius and me are pleased to announce that Expi2Java 1.6 was released two days ago. And by the way, Alex has recently finished his MSc and is looking for a job in industry. If you know anything interesting in a German or English speaking country, please let him know.

Expi2Java 1.6 was released yesterday (11.05.2011)

The highlights of this release are the new symbolic library and a mechanized formalization in Coq.

The symbolic library abstracts away cryptographic primitives as symbolic terms and networking as pi-calculus-like channels. It is designed to be sound and simple enough to simplify proving the transformation secure. Both the symbolic and concrete libraries can be used interchangeably with all provided examples.

We have formalized the transformation from Expi Calculus to a subset of Java performed by Expi2Java using the Coq proof assistant and proved the symbolic library and the produced Java code to be well-typed. The formalization and all proofs can be found on the project homepage.

The full list of changes: Read the rest of this entry »

DVerify 1.0 released

September 23, 2010

DVerify is a new tool for verifying Dminor programs. It achieves pretty much the same thing as the Dminor type-checker, just in a quite different way: DVerify translates Dminor programs into a quite standard while language, and then uses the Boogie generic verification condition generator backend to verify the translated program. The soundness of this technique has been proved formally using Coq. DVerify and the Coq proofs are the product of Thorsten Tarrach’s recently defended Master’s thesis.

zk-typechecker 0.2.0 Released

February 12, 2009

The zero-knowledge type-checker is a tool for automatically analyzing the security of protocols that use zero-knowledge proofs. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. The type-checker relies on the SPASS (or E) automated theorem prover to discharge proof obligations. It is released under the terms of the Apache License.

This release of the zero-knowledge type-checker adds support for security despite compromise and fixes many of the issues in the initial release (release notes). You can grab it from the page of the project.

The Debian Patch for OpenSSL

May 16, 2008

A Slashdot comment linked to this very interesting post by a Debian developer on the openssl-dev list:

“What I currently see as best option is to actually comment out those 2 lines of code. But I have no idea what effect this really has on the RNG. The only effect I see is that the pool might receive less entropy. But on the other hand, I’m not even sure how much entropy some unitialised data has.

What do you people think about removing those 2 lines of code?”

This change made all keys generated over the last 2 years on any machine running Debian (or a derivative) be extremely easily guessable. Not only should you regenerate all your keys as soon as possible if affected, but if somebody recorded sensitive traffic you did in the last two years then you are in deep deep trouble.

Why on earth are the Debian developers patching security-critical packages without having absolutely any clue about the implications? How many other vulnerabilities did they actually introduce in this way?

Google Summer of Code 2008

March 27, 2008

Student applications are now open 🙂


Producing Open Source Software

January 31, 2008

If you want to learn how to successfully manage an open source project then you should definitely read Producing Open Source Software, by Karl Fogel. The book is published by O’Reilly and is available under a Creative Commons license.

Producing Open Source

Skype Plugin for Gaim/Pidgin/Adium

December 5, 2007

The URL: http://www.myjobspace.co.nz/images/pidgin/

The good. This is a plugin many people (me included) have been waiting for years. Most important, it allows you to have all your buddies in one place, and communicate with them in a stemless way (no matter whether they use GTalk, Yahoo!, AIM, ICQ, MSN, IRC, or whatever). This has always been one of the biggest advantages of using Gaim/Pidgin/Adium. But there was still one important protocol which it could not do, because the developers of this protocol tried their very best to make this impractical: Skype. Still, a while ago, in a sudden outbreak of common sense, the Skype developers released a public API, which now made this plugin possible.

The bad. The plugin requires Skype to be running as it uses the Skype public API to communicate with a running copy of Skype. This is needed since reverse-engineering the evil Skype protocol, while not impossible, would be a daunting task (see Silver Needle in the Skype for more details about this).

Many people are using Gaim/Pidgin/Adium because it is Free Software (GPL). It is also running in more or less the same way on any operating system. This is particularly interesting for people using proprietary instant messaging clients on non-Windows machines, because they had to stick with much older versions (while for Windows, Skype is at version 3.6, for Linux it is at 1.4 and for Mac at 2.6), this assuming there was some version for their operating system. These are problems that the current plugin can unfortunately not fix, since it relies on a running (proprietary and possible outdated) copy of Skype. Still, the plugin itself is GPL.

The uggly. No voice or video support, but this is a general problem with Gaim/Pidgin/Adium, which will only get solved if someone is willing to invest some time into it. The plugin itself worked fine for me so far with Adium, even though there are some Known Issues (see readme).

Related (good) news: GTalk now interoperates with AIM and ICQ.