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