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@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@15: Identifier : string, 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