Formal Specification and Verification

[Dan Palmer]

Hi everyone,

I've been reading some of the messages here and it seems everyone likes the idea of starting from code and formulating the concepts of the framework through coding it. As someone who has had to work with OAuth 1 and 2, it's good to see this approach being taken, and I hope it will result in a framework that is much nicer for software engineers to use.

However I can see two possible issues with this  and I would appreciate it if you could give me a few answers.

1. At the end of the day, us writing these systems doesn't really matter. If it takes us a few days to better understand a technology, that's annoying for us, but a system that confuses users making it more difficult for them will cause a large amount more 'damage'. Will there be a focus on the end result for the user? I think very few sacrifices are worth making to make development easier.

2. What's going to happen with formal specification and verification? OAuth has an RFC spec, and went through the process of peer review for that. Is that the plan with this framework? If so, at what stage can we expect to see a draft specification that isn't just code. As well as this, are there any plans to perform formal verification of the system in the way that happened with OAuth (Pai, Sharma et al 2011). It might be good to do this along with the draft coding in order to verify the security of the system.

Thanks in advance for answers, interested to hear what you think of these issues.

[Eran Hammer]

The end-user experience isn’t going to be dramatically different from OAuth. I hope to innovate in the mobile app space but initially it will be limited to what has already been tried out in the industry.

 

As for a specification, I have no intention or interest in ever writing one. I’m providing this as an open source library. Others are welcome to do with it as they please. I’m writing it because I need it, and I’m doing it as open source in order to solicit feedback and improve it.

 

EH

--
 
 

[Eran Hammer]

OAuth 2 stripped down, with OAuth 1 signature protection, optimized for mobile/native.

You should be familiar with OAuth 1 or 2 to have a good grip of Oz.

EH

-----Original Message-----
From: algermissen1971 [mailto:algermi...@me.com]
Sent: Friday, November 23, 2012 1:50 PM
To: Eran Hammer
Cc: oz-pr...@googlegroups.com
Subject: Re: Formal Specification and Verification

Hi Eran,

On Nov 6, 2012, at 6:28 PM, Eran Hammer <er...@hueniverse.com> wrote:

> The end-user experience isn't going to be dramatically different from OAuth

What reading do you suggest to help me understand what you are up to with OZ?

I would very much like to follow your implementation, but I lack the sufficient understanding so much that I do not even know where to start, really.

Sould I be thinking

'OZ is sort of OAuth1 done better'

or

'OZ is like BigCoVariantX of OAuth2 with client certs and no Open ID Connect or SAML'

or is it too different from both to use eany of the existing docs to help me understand your coding.

Is there a time period of OAuth2 WG Archives that you think is educational to dig through?


Jan