diff src/ur/openid.urs @ 15:35bc4da563dd

Realms; documentation and license
author Adam Chlipala <adam@chlipala.net>
date Sun, 02 Jan 2011 11:22:30 -0500
parents de04a3fc6b72
children f6b3fbf10dac
line wrap: on
line diff
--- a/src/ur/openid.urs	Sun Jan 02 10:33:07 2011 -0500
+++ b/src/ur/openid.urs	Sun Jan 02 11:22:30 2011 -0500
@@ -1,16 +1,124 @@
+(* This module implements the key primitive of the OpenID 2.0 authentication
+ * protocol, as specified in:
+ *   http://specs.openid.net/auth/2.0
+ *
+ * Module author: Adam Chlipala
+ *
+ * Known missing features:
+ * - Compatibility with prior OpenID protocols
+ * - Endpoint discovery via XRIs or Yadis
+ * - Immediate requests (authentication with no opportunity for user
+ *   interaction)
+ * - Publishing information for relying party discovery
+ * - Extensions (in the protocol specification's terminology)
+ *
+ * Support for every other aspect of relying party functionality should be
+ * present, including appropriate security measures.
+ *)
+
+(* == Quick summary of OpenID ==
+ * There are lots of protocol details, but my take on it comes down to one
+ * simple idea.  OpenID exports a primitive that allows a web site that verify
+ * that a particular _user_ wishes to provide his identity to a particular
+ * _URL_.  There is use of cryptography and other fanciness to implement this
+ * primitive securely and efficiently, but application builders shouldn't need
+ * to think about the implementation details.  Indeed, that simple interface is
+ * what this module exports.  Thanks to Ur/Web's usual encapsulation guarantees,
+ * client code need not worry about accidentally disturbing state used by the
+ * protocol.
+ *
+ * The last key aspect is that URLs are used to identify users.  Each URL should
+ * point to an HTML page containing a special tag which points to another URL
+ * that is assigned responsibility for answering queries about what the user
+ * has authorized.  To use the library, you only need to think about the
+ * initial, user-identifying URLs, which form a kind of universal username
+ * namespace.
+ *)
+
+(* The protocol provides some options for how particular security requirements
+ * can be satisfied.  This module defines a few datatypes for the different
+ * dimensions of choice. *)
+
+(* First, we have association types, which are methods of guaranteeing message
+ * integrity.  The only options in OpenID 2.0 are two different hash-based
+ * message authentication codes (HMACs).  [HMAC_SHA256] is the stronger
+ * scheme. *)
+
 datatype association_type = HMAC_SHA1 | HMAC_SHA256
+
+(* Next, there are association session types, which are approaches to
+ * establishing shared secrets that can be used to provide integrity.  There are
+ * two versions of the Diffie-Hellman key exchange protocol, based on pairing
+ * with different MAC algorithms.  The [NoEncryption] option is only
+ * appropriate for communication via SSL, which already provides secrecy.  If
+ * [NoEncryption] is requested over an unencrypted HTTP connection, the library
+ * will automatically switch to [DH_SHA256]. *)
+
 datatype association_session_type = NoEncryption | DH_SHA1 | DH_SHA256
+
+(* Finally, you have the option to skip all this crypto stuff in your
+ * application, at some expense.  Use of cryptography with shared secrets allows
+ * you to authenticate a user with one fewer round-trip to the remote web server
+ * that is placed in charge of that user's identity.  This benefit is traded for
+ * greater space requirements in your application, with several kinds of data
+ * stored in local SQL tables, with the number of rows roughly proportional to
+ * the number of authentications, over short time periods.  A stateless approach
+ * uses local state only as a cache for predictable HTTP request results, with
+ * storage use proportional to the number of users.  (The stateful approach uses
+ * that same state and more.) *)
+
 datatype association_mode =
          Stateless
        | Stateful of {AssociationType : association_type,
                       AssociationSessionType : association_session_type}
 
-datatype authentication = AuthenticatedAs of string | Canceled | Failure of string
+(* An authentication attempt terminates in one of four ways.
+ * First, the user might get bored and surf away, never finishing the process.
+ * If so, your application will never be told explicitly.
+ * The other possibilities are captured by this datatype: *)
+
+datatype authentication =
+         AuthenticatedAs of string
+         (* Successful authentication, with the user's verified identifying
+          * URL *)
+       | Canceled
+         (* The user explicitly canceled the authentication process. *)
+       | Failure of string
+         (* Something went wrong, and here's some text that hopefully diagnoses
+          * the problem. *)
+
+(* Finally, here's the function to call to verify that a user wants to
+ * authenticate to your particular web application.  Note that this will only
+ * work properly if your project .urp file includes a 'prefix' directive that
+ * gives the full protocol, hostname, and port part of your URLs.
+ *
+ * If authentication proceeds successfully, the function will never return.
+ * Instead, the user is redirected to his identity provider, to authenticate with
+ * whatever method they have agreed on.  When that process finishes, the user is
+ * redirected back to your app, at which time the function that you pass as the
+ * first argument below is called with the result, to generate the page to show
+ * to the user.
+ *
+ * If authentication fails before the user is redirected away, the original
+ * function returns an error message suitable for display to technically-savvy
+ * users. *)
 
 val authenticate : (authentication -> transaction page)
                    -> {Association : association_mode,
-                       Identifier : string}
+                       (* Your preferences for statefulness and cryptography.
+                        * If the remote server doesn't support some kind of
+                        * crypto that you ask for, the library automatically
+                        * switches to a mode that the server advertises as
+                        * supported. *)
+                       Identifier : string,
+                       (* The URL that the user claims identifies him.
+                        * It may also point to a generic authentication service
+                        * that will take care of deciding the proper
+                        * username. *)
+                       Realm : option string
+                       (* A URL prefix that we are asking the user to authorize.
+                        * If provided, it must be a genuine prefix of every
+                        * application URL.  If omitted, we authorize for just one
+                        * specific URL, which is the authentication-specific URL
+                        * that the library always chooses automatically. *)}
                    -> transaction string
-(* Doesn't return normally if everything goes as planned.
- * Instead, the user is redirected to his OP to authenticate there.
- * Later, the function passed as the first argument should be called with the result. *)