|
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
|
