annotate src/ur/openid.urs @ 55:1ceea714b3b5

Merge from upstream.
author Karn Kallio <kkallio@eka>
date Tue, 19 Jul 2011 11:03:29 -0430
parents f6b3fbf10dac
children
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@39 75 (* It is possible to request authentication in two different modes: *)
adam@39 76
adam@39 77 datatype authentication_mode =
adam@39 78 ChooseIdentifier of string
adam@39 79 (* The provider prompts the user to select his identity.
adam@39 80 * The string argument should be a generic endpoint, e.g.,
adam@39 81 * "https://www.google.com/accounts/o8/id". *)
adam@39 82 | KnownIdentifier of string
adam@39 83 (* Require authentication as this precise identifier. *)
adam@39 84
adam@15 85 (* An authentication attempt terminates in one of four ways.
adam@15 86 * First, the user might get bored and surf away, never finishing the process.
adam@15 87 * If so, your application will never be told explicitly.
adam@15 88 * The other possibilities are captured by this datatype: *)
adam@15 89
adam@15 90 datatype authentication =
adam@15 91 AuthenticatedAs of string
adam@15 92 (* Successful authentication, with the user's verified identifying
adam@15 93 * URL *)
adam@15 94 | Canceled
adam@15 95 (* The user explicitly canceled the authentication process. *)
adam@15 96 | Failure of string
adam@15 97 (* Something went wrong, and here's some text that hopefully diagnoses
adam@15 98 * the problem. *)
adam@15 99
adam@15 100 (* Finally, here's the function to call to verify that a user wants to
adam@15 101 * authenticate to your particular web application. Note that this will only
adam@15 102 * work properly if your project .urp file includes a 'prefix' directive that
adam@15 103 * gives the full protocol, hostname, and port part of your URLs.
adam@15 104 *
adam@15 105 * If authentication proceeds successfully, the function will never return.
adam@15 106 * Instead, the user is redirected to his identity provider, to authenticate with
adam@15 107 * whatever method they have agreed on. When that process finishes, the user is
adam@15 108 * redirected back to your app, at which time the function that you pass as the
adam@15 109 * first argument below is called with the result, to generate the page to show
adam@15 110 * to the user.
adam@15 111 *
adam@15 112 * If authentication fails before the user is redirected away, the original
adam@15 113 * function returns an error message suitable for display to technically-savvy
adam@15 114 * users. *)
adam@8 115
adam@10 116 val authenticate : (authentication -> transaction page)
adam@13 117 -> {Association : association_mode,
adam@15 118 (* Your preferences for statefulness and cryptography.
adam@15 119 * If the remote server doesn't support some kind of
adam@15 120 * crypto that you ask for, the library automatically
adam@15 121 * switches to a mode that the server advertises as
adam@15 122 * supported. *)
adam@39 123 Identifier : authentication_mode,
adam@15 124 (* The URL that the user claims identifies him.
adam@15 125 * It may also point to a generic authentication service
adam@15 126 * that will take care of deciding the proper
adam@15 127 * username. *)
adam@15 128 Realm : option string
adam@15 129 (* A URL prefix that we are asking the user to authorize.
adam@15 130 * If provided, it must be a genuine prefix of every
adam@15 131 * application URL. If omitted, we authorize for just one
adam@15 132 * specific URL, which is the authentication-specific URL
adam@15 133 * that the library always chooses automatically. *)}
adam@10 134 -> transaction string