a semi-formalization of of the openid protocol

[Imran Ghory]

I've produced a semi-formalization of the protocol used stripping out
the implementation details so it's easier to analyze from a
security/efficency viewpoint as well as providing an alternative
explaination to the main spec page to help focus on any points that
may be open to misinterpretation.

If someones bored they can take the formalization a bit further and
try attacking the protocol using something like BAN logic to try and
find vulnerabilites.  I also plan to go through my formalization and
try and produce justification for every piece of info sent/recieved to
try and help improve the understanding of why the protocol is designed
like it is.

The format I've used is

Source
---------> Information being sent
Destination.

I've used various other bits of notation (for example information
being sent is prefixed by the name of whoever generated the data so
the flow of information can be seen) but hopefully it's mostly
self-explanatory.

So here it is:

User 
---------> User_server_url
Consumer


Consumer
---------> User_server_url
---------> Consumer_Request_for_id_server_url
User-site


User-site
---------> User-site_id_server_url
Consumer


Consumer
---------> User-site_id_server_url
---------> consumer_nonce
---------> consumer_return_to_url
---------> consumer_trust_root_url
---------> user_server_url
User


User
---------> consumer_nonce
---------> consumer_return_to_url
---------> consumer_trust_root_url
---------> user_server_url
id-server


id-server
---------> user_server_url
---------> consumer_return_to_url
---------> consumer_nonce
---------> id-server_timestamp
---------> id-server_signed
--------->              (id-server_timestamp, 
--------->               user_server_url, 
--------->               consumer_return_to_url,
--------->               consumer nonce)
User


User
---------> user_server_url
---------> consumer_return_to_url
---------> consumer_nonce
---------> id-server_timestamp
---------> id-server_signed
--------->              (id-server_timestamp, 
--------->               user_server_url, 
--------->               consumer_return_to_url,
--------->               consumer nonce)
Consumer


Any questions/mistakes/whatever welcome.

Imran