Anonymous connections and onion routing

Onion routing is an infrastructure for private communication over a public network. It provides anonymous connections that are strongly resistant to both eavesdropping and traffic analysis. Onion routing's anonymous connections are bidirectional, near real-time, and can be used anywhere a socket connection can be used. Any identifying information must be in the data stream carried over an anonymous connection. An onion is a data structure that is treated as the destination address by onion routers; thus, it is used to establish an anonymous connection. Onions themselves appear different to each onion router as well as to network observers. The same goes for data carried over the connections they establish. Proxy-aware applications, such as Web browsers and e-mail clients, require no modification to use onion routing, and do so through a series of proxies. A prototype onion routing network is running between our lab and other sites. This paper describes anonymous connections and their implementation using onion routing. This paper also describes several application proxies for onion routing, as well as configurations of onion routing networks     

An alternative method for treating buccal osseous defects

This case demonstrates the successful use of a hydroxylapatite block for maintenance of ridge contour. The procedure offers an alternative to guided tissue regeneration for treating osseous defects of the buccal cortical plate, which may occur following tooth extraction.     

Temporarily hidden bit commitment and lottery applications

This paper describes various types of commitment functions that maintain a secret for a predictable time delay or until a moderate and predictable amount of computation has occurred. The properties we set out for such functions are based on their usefulness for various applications, such as publicly verifiable lotteries, rather than for cryptologic investigation of the functions. In these lotteries, winners are chosen fairly using only internal information. Since all this information may be published (even before the lottery closes), anyone can do the calculation and therefore verify that the winner was chosen correctly. Since the calculation uses a delaying or similar function, neither ticket purchasers nor the lottery organizer can take advantage of this information. We describe several such lotteries and the security requirements they satisfy, assuming that functions with the properties we state are used.     

Mechanically verifying concurrent programs with the Boyer-Mooreprover

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree     

A Mechanization of Unity in PC-NQTHM-92

This paper presents in detail how the Unity logic for reasoning about concurrent programs was formalized within the mechanized theorem prover PC-NQTHM-92. Most of Unitys proof rules were formalized in the unquantified logic of NQTHM, and the proof system has been used to mechanically verify several concurrent programs. The mechanized proof system is sound by construction, since Unitys proof rules were proved about an operational semantics of concurrency, also presented here. Skolem functions are used instead of quantifiers, and the paper describes how proof rules containing Skolem function are used instead of Unitys quantified proof rules when verifying concurrent programs. This formalization includes several natural extensions to Unity, including nondeterministic statements. The paper concludes with a discussion of the cost and value of mechanization.