Mercurial > openid
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. *) |