A Cryptol Implementation of Skein

Following on from the MD6-in-Cryptol posting, let's consider another very interesting candidate from the (deep) pool of SHA-3 submissions; Skein 

 http://www.skein-hash.info/ http://www.schneier.com/skein.html

by the merry band of Ferguson, Lucks, Schneier, et al.The expression of their reference implementation comes out, we think, fairly cleanly in Cryptol. The digest output size is a variable parameter to the algorithm, but we'll focus on the 512-bit version here -- the submission's primary candidate for SHA-3.In order to avoid duplicating the introductory material on Cryptol, we suggest the reader go through the MD6 writeup to get a grounding in Cryptol, its idioms, and syntax.

Click to read more ...

MD6 in Cryptol

NIST is currently running a competition to come up with the next generation message hashing function that it intends to standardize and FIPS recommend upon completion (assuming one good candidate is left standing and well at the conclusion of the evaluation process):

 http://csrc.nist.gov/groups/ST/hash/sha-3/index.html

Apart from the need to come up with better alternatives to its current recommendation, the SHA-2 family of hashing functions, this competition draws inspiration from the success that the AES competition had a couple of years ago in engaging the community in coming up with a replacement for the DES block cipher. As then, a lot of new innovation has resulted.As with block ciphers, many common types of hashing functions lend themselves well to expression in Cryptol. To demonstrate some of the features of Cryptol and how it could be used to express SHA-3 candidates, here's one of the submissions, MD6 from the CSAIL group at MIT, headed by Ronald L. Rivest:

 http://groups.csail.mit.edu/cis/md6/

The goal of this writeup is twofold:

• Introduce you to the MD6 hashing algorithm and its construction.


• Expose you to the Cryptol language, and how it lends itself to expressing MD6.

Ideally, you'll come away with enthusiasm on both accounts!

Click to read more ...

Rosetta feature in IEEE Computer

If you get IEEE Computer, check out the article on page 108 of the January, 2009 issue: Rosetta: Standardization at the System Level.  The author, Perry Alexander , is a professor at the University of Kansas.  Perry describes Rosetta, a language for designing and modeling systems.  The language is undergoing IEEE standardization, and there's even a book describing the language.Perry collaborates with me and others at Galois, Inc. and has used Rosetta on one of our joint formal methods projects.

Click to read more ...

Tech Talk: Android G1: Experiences with an open mobile platform

The second Galois Tech Talk, for 2009, was Isaac Potoczny-Jones (aka SyntaxNinja) on developing for the Android G1 phone. You can read the slides..

The Android G1 is a TMobile phone whose operating system, Android is based on Linux and was developed by Google. It's a very open smart-phone platform that rivals the iPhone.While I'm no expert in Android or mobile platform development, I will discuss my experiences in Android development and demonstrate the toolchain used to develop software for the Android. I'll outline the basic features of the platform, with a focus on the factors that make its openness so powerful:* the inter-process communications mechanism whereby applications can advertise the services they offer and other applications can take advantage of those services,* The open-source Java, Eclipse, and Linux-based toolchain,* the OpenIntents project.This will be an informal demonstration and discussion.A group of us in collaboration between the Android Password Safe project and the Openintents project have implemented a cryptography service and a keystore service which other Android applications can use to keep data and passwords safe, in a way that's convenient for the end user.Our system allows a single password, and periodic single sign-on so that all applications can encrypt, decrypt, and store keys using the same master password that the user enters once.

• Date: Tuesday, January 20, 2008
• Time: 10:30am - 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

Click to read more ...

Galois at POPL

The Principles of Programming Languages conference, POPL 09, and its surrounding workshops is kicking off this week in Savannah, Georgia. Galwegians will be attending most of the conferences: you might be able to find Levent at VMCAI or the Twelf Tutorial, or Iavor at TLDI or POPL, and Jeff Lewis (now at Signali) will be giving a keynote at PADL. Step up and say "hello!".

Click to read more ...