annotate 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
rev   line source
adam@15 1 (* This module implements the key primitive of the OpenID 2.0 authentication
adam@15 2 * protocol, as specified in:
adam@15 3 * http://specs.openid.net/auth/2.0
adam@15 4 *
adam@15 5 * Module author: Adam Chlipala
adam@15 6 *
adam@15 7 * Known missing features:
adam@15 8 * - Compatibility with prior OpenID protocols
adam@15 9 * - Endpoint discovery via XRIs or Yadis
adam@15 10 * - Immediate requests (authentication with no opportunity for user
adam@15 11 * interaction)
adam@15 12 * - Publishing information for relying party discovery
adam@15 13 * - Extensions (in the protocol specification's terminology)
adam@15 14 *
adam@15 15 * Support for every other aspect of relying party functionality should be
adam@15 16 * present, including appropriate security measures.
adam@15 17 *)
adam@15 18
adam@15 19 (* == Quick summary of OpenID ==
adam@15 20 * There are lots of protocol details, but my take on it comes down to one
adam@15 21 * simple idea. OpenID exports a primitive that allows a web site that verify
adam@15 22 * that a particular _user_ wishes to provide his identity to a particular
adam@15 23 * _URL_. There is use of cryptography and other fanciness to implement this
adam@15 24 * primitive securely and efficiently, but application builders shouldn't need
adam@15 25 * to think about the implementation details. Indeed, that simple interface is
adam@15 26 * what this module exports. Thanks to Ur/Web's usual encapsulation guarantees,
adam@15 27 * client code need not worry about accidentally disturbing state used by the
adam@15 28 * protocol.
adam@15 29 *
adam@15 30 * The last key aspect is that URLs are used to identify users. Each URL should
adam@15 31 * point to an HTML page containing a special tag which points to another URL
adam@15 32 * that is assigned responsibility for answering queries about what the user
adam@15 33 * has authorized. To use the library, you only need to think about the
adam@15 34 * initial, user-identifying URLs, which form a kind of universal username
adam@15 35 * namespace.
adam@15 36 *)
adam@15 37
adam@15 38 (* The protocol provides some options for how particular security requirements
adam@15 39 * can be satisfied. This module defines a few datatypes for the different
adam@15 40 * dimensions of choice. *)
adam@15 41
adam@15 42 (* First, we have association types, which are methods of guaranteeing message
adam@15 43 * integrity. The only options in OpenID 2.0 are two different hash-based
adam@15 44 * message authentication codes (HMACs). [HMAC_SHA256] is the stronger
adam@15 45 * scheme. *)
adam@15 46
adam@8 47 datatype association_type = HMAC_SHA1 | HMAC_SHA256
adam@15 48
adam@15 49 (* Next, there are association session types, which are approaches to
adam@15 50 * establishing shared secrets that can be used to provide integrity. There are
adam@15 51 * two versions of the Diffie-Hellman key exchange protocol, based on pairing
adam@15 52 * with different MAC algorithms. The [NoEncryption] option is only
adam@15 53 * appropriate for communication via SSL, which already provides secrecy. If
adam@15 54 * [NoEncryption] is requested over an unencrypted HTTP connection, the library
adam@15 55 * will automatically switch to [DH_SHA256]. *)
adam@15 56
adam@8 57 datatype association_session_type = NoEncryption | DH_SHA1 | DH_SHA256
adam@15 58
adam@15 59 (* Finally, you have the option to skip all this crypto stuff in your
adam@15 60 * application, at some expense. Use of cryptography with shared secrets allows
adam@15 61 * you to authenticate a user with one fewer round-trip to the remote web server
adam@15 62 * that is placed in charge of that user's identity. This benefit is traded for
adam@15 63 * greater space requirements in your application, with several kinds of data
adam@15 64 * stored in local SQL tables, with the number of rows roughly proportional to
adam@15 65 * the number of authentications, over short time periods. A stateless approach
adam@15 66 * uses local state only as a cache for predictable HTTP request results, with
adam@15 67 * storage use proportional to the number of users. (The stateful approach uses
adam@15 68 * that same state and more.) *)
adam@15 69
adam@13 70 datatype association_mode =
adam@13 71 Stateless
adam@13 72 | Stateful of {AssociationType : association_type,
adam@13 73 AssociationSessionType : association_session_type}
adam@13 74
adam@15 75 (* An authentication attempt terminates in one of four ways.
adam@15 76 * First, the user might get bored and surf away, never finishing the process.
adam@15 77 * If so, your application will never be told explicitly.
adam@15 78 * The other possibilities are captured by this datatype: *)
adam@15 79
adam@15 80 datatype authentication =
adam@15 81 AuthenticatedAs of string
adam@15 82 (* Successful authentication, with the user's verified identifying
adam@15 83 * URL *)
adam@15 84 | Canceled
adam@15 85 (* The user explicitly canceled the authentication process. *)
adam@15 86 | Failure of string
adam@15 87 (* Something went wrong, and here's some text that hopefully diagnoses
adam@15 88 * the problem. *)
adam@15 89
adam@15 90 (* Finally, here's the function to call to verify that a user wants to
adam@15 91 * authenticate to your particular web application. Note that this will only
adam@15 92 * work properly if your project .urp file includes a 'prefix' directive that
adam@15 93 * gives the full protocol, hostname, and port part of your URLs.
adam@15 94 *
adam@15 95 * If authentication proceeds successfully, the function will never return.
adam@15 96 * Instead, the user is redirected to his identity provider, to authenticate with
adam@15 97 * whatever method they have agreed on. When that process finishes, the user is
adam@15 98 * redirected back to your app, at which time the function that you pass as the
adam@15 99 * first argument below is called with the result, to generate the page to show
adam@15 100 * to the user.
adam@15 101 *
adam@15 102 * If authentication fails before the user is redirected away, the original
adam@15 103 * function returns an error message suitable for display to technically-savvy
adam@15 104 * users. *)
adam@8 105
adam@10 106 val authenticate : (authentication -> transaction page)
adam@13 107 -> {Association : association_mode,
adam@15 108 (* Your preferences for statefulness and cryptography.
adam@15 109 * If the remote server doesn't support some kind of
adam@15 110 * crypto that you ask for, the library automatically
adam@15 111 * switches to a mode that the server advertises as
adam@15 112 * supported. *)
adam@15 113 Identifier : string,
adam@15 114 (* The URL that the user claims identifies him.
adam@15 115 * It may also point to a generic authentication service
adam@15 116 * that will take care of deciding the proper
adam@15 117 * username. *)
adam@15 118 Realm : option string
adam@15 119 (* A URL prefix that we are asking the user to authorize.
adam@15 120 * If provided, it must be a genuine prefix of every
adam@15 121 * application URL. If omitted, we authorize for just one
adam@15 122 * specific URL, which is the authentication-specific URL
adam@15 123 * that the library always chooses automatically. *)}
adam@10 124 -> transaction string