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