1,058 research outputs found
Provably correct Java implementations of Spi Calculus security protocols specifications
No full textSpi Calculus is an untyped high level modeling language for security protocols, used for formal protocols specification and verification. In this paper, a type system for the Spi Calculus and a translation function are formally defined, in order to formalize the refinement of a Spi Calculus specification into a Java implementation. The Java implementation generated by the translation function uses a custom Java library. Formal conditions on such library are stated, so that, if the library implementation code satisfies such conditions, then the generated Java implementation correctly simulates the Spi Calculus specification. A verified implementation of part of the custom library is further presente
Spontaneous otoacoustic emissions and relaxation dynamics of long decay time OAEs in audiometrically normal and impaired subjects
No full textThe relationship between hearing loss, detected by measuring the audiometric threshold shift, and the presence of long-lasting otoacoustic emissions, has been studied in a population of 66 adult males, by analyzing the cochlear response in the 80 ms following the subministration of a click stimulus. Most long-lasting OAEs are also recognizable as Synchronized Spontaneous OAEs (SSOAEs). The OAE characteristic decay times were evaluated according to the model by Sisto and Moleti [J. Acoust. Sec. Am. 106, 1893 (1999)]. The starting hypothesis, confirmed by the results, is that long decay time and large equilibrium amplitude are both manifestations of the effectiveness of the active feedback mechanism. The prevalence and frequency distribution of long-lasting OAEs, and of their SSOAE subset, have been separately analyzed for normal and impaired ears. No long-lasting OAE was found within the hearing loss frequency range, but several were found in impaired ears outside the hearing loss range, both at lower and higher frequencies. This result suggests that the correlation between the presence of long-lasting OAEs and good cochlear functionality be local in the frequency domain. The monitor of the OAE decay time is proposed as a new possible method for early detecting hearing loss in populations exposed to noise. (C) 2001 Acoustical Society of America
An Experiment in Interoperable Cryptographic Protocol Implementation Using Automatic Code Generation
No full textSpi2Java is a tool that enables semi-automatic generation of cryptographic protocol implementations, starting from verified formal models. This paper shows how the last version of spi2Java has been enhanced in order to enable interoperability of the generated implementations. The new features that have been added to spi2Java are reported here. A case study on the SSH transport layer protocol, along with some experiments and measures on the generated code, is also provided. The case study shows, with facts, that reliable and interoperable implementations of standard security protocols can indeed be obtained by using a code generation tool like spi2Jav
Does the "reticular lamina nonlinearity" contribute to the basal DPOAE source?
No full textThe spatial extent of the cochlear region that actually contributes to the DPOAE signal measured in the ear canal may be evaluated experimentally using interference tones or computed numerically using nonlinear cochlear models. A nonlinear transmission-line cochlear model is used in this study to evaluate whether the recently reported nonlinear behavior of the reticular lamina (RL) over a wide basal region may be associated with generation of a significant distortion product otoacoustic emission (DPOAE) component. A two-degrees-of-freedom 1-D nonlinear model was used as discussed by Sisto et al. (2019), in which each local element consists of two coupled oscillators, roughly representing the basilar membrane (BM) and the RL. In this model, the RL shows a strongly nonlinear response over a wide region basal to the characteristic place, whereas the BM response is linear outside the narrow peak region. Such a model may be considered as that using the minimal number of degrees of freedom necessary to separately predict the motion of the BM and RL, while preserving important cochlear symmetries, such as the zero-crossing invariance of the impulse response. In the numerical simulations, the RL nonlinearity generates indeed a large intracochlear distortion product source, extended down to very basal cochlear regions. Nevertheless, due to the weak and indirect coupling between the RL motion and the differential fluid pressure in the basal part of the traveling wave path, no significant contribution from this mechanism is predicted by the model to the generation of the DPOAE signal that is eventually measured in the ear canal
Safe abstractions of data encodings in formal security protocol models
No full textWhen using formal methods, security protocols are usually modeled at a high level of abstraction. In particular, data encoding and decoding transformations are often abstracted away. However, if no assumptions at all are made on the behavior of such transformations, they could trivially lead to security faults, for example leaking secrets or breaking freshness by collapsing nonces into constants. In order to address this issue, this paper formally states sufficient conditions, checkable on sequential code, such that if an abstract protocol model is secure under a Dolev-Yao adversary, then a refined model, which takes into account a wide class of possible implementations of the encoding/decoding operations, is implied to be secure too under the same adversary model. The paper also indicates possible exploitations of this result in the context of methods based on formal model extraction from implementation code and of methods based on automated code generation from formally verified model
Knowledge Diffusion and Networking in the Organic Production Sector: A Case Study
No full textKnowledge Diffusion and Networking in the Organic Production Sector: A Case Study Copyright The Agricultural Ecomomics Society and the European Association of Agricultural Economists 2006.
Modeling otoacoustic emissions by active nonlinear oscillators
No full textThe phenomenology of Spontaneous otoacoustic emissions (OAEs) is compared to theoretical predictions given by models in which they are produced by active nonlinear oscillators. Along with the well-known Van der Pol oscillator, a new active oscillator model is proposed and analyzed here. Numerical simulations and multi-scale analytical computation results are compared to experimental data of neonatal spontaneous and evoked OAEs. A simple analysis technique is proposed, in which the time evolution after a click stimulus of the amplitude of each spectral line corresponding to a spontaneous OAE is studied. Apart from a few stationary lines, an approximately exponential decay law, with characteristic damping coefficients in the 20-200 Hz range, was found to fit the data. These results are not compatible with a Van der Pol oscillator model, and show that some important aspects of the OAE phenomenology can be better explained by the proposed oscillator. Other interesting features of the spontaneous end evoked OAE phenomenology, such as spontaneous OAE suppression by external tones and the following recovery, as well as stimulus/response curves in the linear and nonlinear mode of acquisition, are also well reproduced by the proposed model. (C) 1999 Acoustical Society of America. [S0001-4966(99)01310-7]
- …
